# Interpolants and Explicit Definitions in Extensions of the Description Logic EL

arXiv: https://arxiv.org/abs/2202.07186 · HTML: https://mlsanity.com/paper/2202.07186/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Feb 2022.

## Built on by (most cited first, 1 of 1)

- [Interpolation in Knowledge Representation](https://mlsanity.com/paper/2512.08833/) (2025)

## Abstract (arXiv)

We show that the vast majority of extensions of the description logic EL do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for EL with nominals, EL with the universal role, EL with a role inclusion of the form rcirc ssqsubseteq s, and for ELI. It follows in particular that the existence of an explicit definition of a concept or individual name cannot be reduced to subsumption checking via implicit definability. We show that nevertheless the existence of interpolants and explicit definitions can be decided in polynomial time for standard tractable extensions of EL (such as EL++) and in ExpTime for ELI and various extensions. It follows that these existence problems are not harder than subsumption which is in sharp contrast to the situation for expressive DLs. We also obtain tight bounds for the size of interpolants and explicit definitions and the complexity of computing them: single exponential for tractable standard extensions of EL and double exponential for ELI and extensions. We close with a discussion of Horn-DLs such as Horn-ALCI.