Tableau-based revision for expressive description logics with individuals

Our understanding of an application domain evolves over time. If we consider an ontology as a set of semantic constraints which describes our understanding of an application domain, ontologies must be revised. Indeed, adding a new semantic constraint to an ontology may make it inconsistent. To restore consistency with minimal loss of semantics, we would change other semantic constraints of the ontology such that the resulting ontology is semantically as close as possible to the initial ontology. To be able to say that an ontology is semantically close to another one, it is needed to define a distance over finite structures representing models, called completion graphs, which characterize the semantics of an ontology. In this paper we present a tableau algorithm for building such completion graphs of an ontology expressed in the description logic SHIQ with individuals. Based on the distance defined over completion graphs, we introduce a revision operation applied to a SHIQ ontology with a set of new semantic constraints. This revision operation computes the completion graphs that a revised ontology should admit. However, there does not always exist an ontology expressible in SHIQ from which a tableau algorithm generates exactly a given set of completion graphs. This leads us to introduce the notion of upper approximation ontology from which a tableau algorithm can generate the smallest set of completion graphs including a given set of completion graphs. This notion allows us to design an algorithm for constructing a revised ontology from an initial ontology with a set of new semantic constraints. We also implement the proposed algorithms with optimizations and report some experimental results to show that a model-based approach to revision of expressive ontologies is practicable.