Deciding inseparability and conservative extensions in the description logic
type: Item
instance of: scholarly article
title: Deciding inseparability and conservative extensions in the description logic
zbMATH Open document ID: 1187.68572
author: Carsten Lutz
author: F. Wolter
published in: Journal of Symbolic Computation
publication date: 2009-12-03T00:00:00Z
review text: 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 q…
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68T30
zbMATH DE Number: 5641698
zbMATH Keywords: description logics
zbMATH Keywords: ontologies
zbMATH Keywords: conservative extension
zbMATH Keywords: modularity
reviewed by: Éric Martin
MaRDI profile type: Publication
full work available at URL: j.jsc.2008.10.007
OpenAlex ID: W2168344789
cites work: A note on the refinement of ontologies
cites work: The Description Logic Handbook
cites work: Q4712659
cites work: Model checking.
cites work: Q3624118
cites work: The Logical Difference Problem for Description Logic Terminologies
cites work: Interpolation in Local Theory Extensions
cites work: Provably Difficult Combinatorial Games
cites work: Q4005196
cites work: Q3971258
DOI: 10.1016/J.JSC.2008.10.007
Recommended article: Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey
Recommended article: Model-theoretic inseparability and modularity of description logic ontologies
Recommended article: Conservative Extensions in the Lightweight Description Logic $\mathcal{EL}$
Recommended article: Reasoning in Description Logics: Basics, Extensions, and Relatives
Recommended article: Decidability of Circumscribed Description Logics Revisited
Recommended article: Conservative Extensions in Horn Description Logics with Inverse Roles
Recommended article: Deciding expressive description logics in the framework of resolution
Recommended article: A Decidable Constructive Description Logic
Recommended article: Q4463936
description: scientific article; zbMATH DE number 5641698