Interpolants and Explicit Definitions in Extensions of the Description Logic EL
share
We show that the vast majority of extensions of the description logic ℰℒ do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for ℰℒ with nominals, ℰℒ with the universal role, ℰℒ with a role inclusion of the form r∘ s⊑ s, and for ℰℒℐ. 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 ℰℒ (such as ℰℒ^++) and in ExpTime for ℰℒℐ 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 ℰℒ and double exponential for ℰℒℐ and extensions. We close with a discussion of Horn-DLs such as Horn-𝒜ℒ𝒞ℐ.
READ FULL TEXT