论文标题
描述逻辑EL的扩展中的插值和明确定义
Interpolants and Explicit Definitions in Extensions of the Description Logic EL
论文作者
论文摘要
我们表明，描述逻辑$ \ mathcal {el} $的绝大多数扩展不享受craig插值或投影性的贝丝可确定性属性。例如，对于带有名义的$ \ Mathcal {el} $，$ \ MATHCAL {EL} $带有通用角色，$ \ Mathcal {el} $，其中包括$ \ r \ circs s \ circ s \ circs sqsubseteq s $，以及$ \ \ nathcal for $ \ \ \ nathcal {eli {eli {eli {eli {eli} $。特别是，尤其是，不能通过隐式确定性将概念或单个名称的显式定义的存在缩小为包含。我们表明，可以在多项式时间内确定插值和明确的定义的存在，用于$ \ MATHCAL {EL} $的标准可拖动扩展（例如$ \ Mathcal {El}^{++} $），在exptime中的exptime和$ \ nathcal {eltacal {elii} $ and Extermentions $ and Extermentions $ and Extermentions $ and exterementions。因此，这些存在问题并不比表达式DLS形成鲜明对比的填充更难。我们还获得了插值和显式定义的大小以及计算它们的复杂性的紧密界限：$ \ Mathcal {el} $的可拖动标准扩展名和$ \ Mathcal {elii} $的单个指数和双向指数。我们通过讨论Horn-dls的讨论，例如horn-$ \ mathcal {alci} $。
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}$.
