Conservative extensions in expressive description logics

TLDR

Conservative extensions are central to ontology design, enabling refinements, safe merges, and modularization, and the core reasoning task is to decide whether one ontology is a conservative extension of another. The study aims to delineate the boundary between expressive description logics where conservativity is decidable and those where it is not. The authors analyze more expressive description logics to map the decidability boundary for conservative extensions. They show that conservative extensions are 2ExpTime‑complete in ALCQI, undecidable in ALCQIO, and already undecidable in ALC when defined model‑theoretically.

Abstract

The notion of a conservative extension plays a central role in ontology design and integration: it can be used to formalize ontology refinements, safe mergings of two ontologies, and independent modules inside an ontology. Regarding reasoning support, the most basic task is to decide whether one ontology is a conservative extension of another. It has recently been proved that this problem is decidable and 2ExpTime-complete if ontologies are formulated in the basic description logic ALC. We consider more expressive description logics and begin to map out the boundary between logics for which conservativity is decidable and those for which it is not. We prove that conservative extensions are 2ExpTime-complete in ALCQI, but undecidable in ALCQIO. We also show that if conservative extensions are defined model-theoretically rather than in terms of the consequence relation, they are undecidable already in ALC.