Conservative Extensions in Horn Description Logics with Inverse Roles
We investigate the decidability and computational complexity of conservative extensions and the related notions of inseparability and entailment in Horn description logics (DLs) with inverse roles. We consider both query conservative extensions, defined by requiring that the answers to all conjunctive queries are left unchanged, and deductive conservative extensions, which require that the entailed concept inclusions, role inclusions, and functionality assertions do not change. Upper bounds for query conservative extensions are particularly challenging because characterizations in terms of unbounded homomorphisms between universal models, which are the foundation of the standard approach to establishing decidability, fail in the presence of inverse roles. We resort to a characterization that carefully mixes unbounded and bounded homomorphisms and enables a decision procedure that combines tree automata and a mosaic technique. Our main results are that query conservative extensions are 2ExpTime-complete in all DLs between ELI and Horn-ALCHIF and between Horn-ALC and Horn-ALCHIF, and that deductive conservative extensions are 2ExpTime-complete in all DLs between ELI and ELHIF_\bot. The same results hold for inseparability and entailment.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
First Order-Rewritability and Containment of Conjunctive Queries in Horn Description Logics
We study FO-rewritability of conjunctive queries in the presence of ontologies formulated in a description logic between EL and Horn-SHIF, along with related query containment problems. Apart from providing characterizat…
Belief Revision, Minimal Change and Relaxation: A General Framework based on Satisfaction Systems, and Applications to Description Logics
Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we pr…
Uniform and Modular Sequent Systems for Description Logics
We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for s…
Reasoning about Typicality and Probabilities in Preferential Description Logics
In this work we describe preferential Description Logics of typicality, a nonmonotonic extension of standard Description Logics by means of a typicality operator T allowing to extend a knowledge base with inclusions of t…
BlockingTractable Reasoning and Conjunctive Query Answering for Defeasible DL-Lite under Rational Closure
In Description Logics (DLs), reasoning under Rational Closure (RC) is a well-known and widely accepted non-monotonic formalism to handle defeasible knowledge. In this paper, we study the application of RC to the core and…