Interpolants and Explicit Definitions in Extensions of the Description Logic EL

TL;DR

This paper investigates the existence and complexity of interpolants and explicit definitions in various extensions of the description logic EL, revealing that most extensions lack certain properties but still allow polynomial or exponential time decision procedures.

Contribution

It demonstrates that interpolant and explicit definition existence can be decided efficiently in many EL extensions, contrasting with the complexity in more expressive DLs.

Findings

Most EL extensions lack Craig interpolation and Beth definability.

Existence of interpolants and explicit definitions is decidable in polynomial or exponential time.

Size bounds for interpolants and definitions are tight, with single or double exponential complexity.

Abstract

We show that the vast majority of extensions of the description logic $\mathcal{EL}$ do not enjoy the Craig interpolation nor the projective Beth definability property. This is the case, for example, for $\mathcal{EL}$ with nominals, $\mathcal{EL}$ with the universal role, $\mathcal{EL}$ with a role inclusion of the form $r\circ s\sqsubseteq s$, and for $\mathcal{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 $\mathcal{EL}$ (such as $\mathcal{EL}^{++}$) and in ExpTime for $\mathcal{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 $\mathcal{EL}$ and double exponential for $\mathcal{ELI}$ and extensions. We close with a discussion of Horn-DLs such as Horn-$\mathcal{ALCI}$.