Deciding inseparability and conservative extensions in the description logic ε L

We study the problem of deciding whether two ontologies are inseparable w.r.t. a signature Sigma, i.e., whether they have the same consequences in the signature Sigma. A special case is to decide whether the extension of an ontology is conservative. By varying the language in which ontologies are formulated and the query language that is used to describe consequences, we obtain different versions of the problem. We focus on the lightweight description logic epsilon L as an ontology language, and consider query languages based on (i) subsumption queries, (ii) instance queries over ABoxes, (iii) conjunctive queries over ABoxes, and (iv) second-order logic. For query languages (i) to (iii), we establish ExpTime-completeness of both inseparability and conservative extensions. Case (iv) is equivalent to a model-theoretic version of inseparability and conservative extensions, and we prove it to be undecidable. We also establish a number of robustness properties for inseparability. (C) 2009 Elsevier Ltd. All rights reserved.