Deciding inseparability and conservative extensions in the description logic (Q1041590)

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.