Did I damage my ontology? A case for conservative extensions in description logic

TLDR

Ontologies are dynamic and often modified by adding axioms or merging, but such changes can have unexpected consequences if the resulting ontology is not a conservative extension of the original. The paper argues that it is essential to determine whether a modified ontology is a conservative extension and proposes new reasoning problems to address this in ALC TBoxes. We analyze conservative extension problems for ALC TBoxes, distinguishing the sizes of the original ontology and added axioms, and present an algorithm that, when non‑conservativeness occurs, computes a witnessing concept. We prove that conservative extension reasoning is decidable and 2EXPTIME‑complete, provide algorithms that are exponential in the original ontology size but double exponential in added axioms, and show that when non‑conservativeness occurs the algorithm computes a minimal‑size witnessing concept, making the complexity comparable to standard reasoning when added axioms are small.

Abstract

In computer science, ontologies are dynamic entities: to adapt them to new and evolving applications, it is necessary to frequently perform modifications such as the extension with new axioms and merging with other ontologies. We argue that, after performing such modifications, it is important to know whether the resulting ontology is a conservative extension of the original one. If this is not the case, then there may be unexpected consequences when using the modified ontology in place of the original one in applications. In this paper, we propose and investigate new reasoning problems based on the notion of conservative extension, assuming that ontologies are formulated as TBoxes in the description logic ALC. We show that the fundamental such reasoning problems are decidable and 2EXPTIME-complete. Additionally, we perform a finer-grained analysis that distinguishes between the size of the original ontology and the size of the additional axioms. In particular, we show that there are algorithms whose runtime is 'only' exponential in the size of the original ontology, but double exponential in the size of the added axioms. If the size of the new axioms is small compared to the size of the ontology, these algorithms are thus not significantly more complex than the standard reasoning services implemented in modern description logic reasoners. If the extension of an ontology is not conservative, our algorithm is capable of computing a concept that witnesses non-conservativeness. We show that the computed concepts are of (worst-case) minimal size.