Deciding inseparability and conservative extensions in the description logic (Q1041590): Difference between revisions

The paper first states the importance, in particular for ontology import and for ontology refinement, of addressing the questions whether two TBoxes \(\mathcal T_1\) and \(\mathcal T_2\) are inseparable with respect to a signature \(\Sigma\), or whether \(\mathcal T_2\) is a conservative extension of \(\mathcal T_1\). The first notion means that \(\mathcal T_1\) and \(\mathcal T_2\) have the same logical consequences expressed in an underlying query language built from \(\Sigma\), and the second notion means that \(\mathcal T_2\) contains \(\mathcal T_1\) and all logical consequences of \(\mathcal T_2\) are logical consequences of \(\mathcal T_1\) in an underlying query language built from the vocabulary from which \(\mathcal T_1\) is defined. For the formal developments, the \(\mathcal{EL}\) description logic is used as the language to define TBoxes, and the main query languages considered are the language \(\mathcal{QL_{EL}}\) of concept inclusions between \(\mathcal{EL}\)-concepts (subsumption queries), the language \(\mathcal{QL}^i_{\mathcal{EL}}\) of whether, given some ABox, a concept name satisfies a concept (instance queries), and the language \(\mathcal{QL}^q_{\mathcal{EL}}\) of whether, given some ABox, a tuple of concept names satisfies an existentially quantified conjunction of concepts and role names (conjunctive queries). It is first shown that for all 3 query languages, the notion of \(\Sigma\)-inseparability enjoys two robustness properties that derive from a counterpart to Craig's interpolation and a counterpart to Robinson consistency property. Then the authors prove that for all 3 query languages, deciding whether two TBoxes are inseparable with respect to a signature and deciding whether one TBox is a conservative extension of the other are ExpTime-complete procedures. The proof techniques make use of simulations between interpretations, canonical models, and a notion of local entailment. The last section focuses on second-order logic used as a query language, and shows that the previous problems are then undecidable. The paper concludes with a number of open questions.