As the size of DL-based ontologies grows, tools that support improving the quality of such ontologies become more important. DL reasoners can be used to detect inconsistencies and to infer other implicit consequences, such as subsumption and instance relationships. However, for the developer of a DL-based ontology, it is often quite hard to understand why a consequence computed by the reasoner actually follows from the knowledge base, and how to repair the ontology in case this consequence is not intended. The classical approach for repairing an ontology first computes all justifications, i.e., minimal subsets of the ontology that have the unintended consequence, and then removes one axiom from each justification. However, removing complete axioms may also eliminate consequences that are still wanted. For example, consider an ontology that contains the following two general concept inclusion axioms (GCIs): Professor v 9employedBy:University u 9enrolledIn:University; 9enrolledIn:University v Student : These two axioms are a justification for the incorrect consequence that professors are students. While the first axiom is the culprit, removing it completely would also remove the correct consequence that professors are employed by a university. Thus, it would be more appropriate to replace the first axiom by the weaker axiom Professor v 9employedBy:University. This is the basic idea underlying our gentle repair approach, in which we weaken one axiom from each justification such that the modified justifications no longer have the consequence. More precisely, the full paper contains the following results: 1. From a semantic point of view, a repair of an ontology O is a new ontology O0 that is implied by O, but does not have the unintended consequence . Such a repair is optimal if there is no repair O00 that strictly implies O0. We show that optimal repairs need not always exist in case O is divided into a strict part (that must not be changed) and a refutable part (that can be changed).
2. Next, we introduce our gentle repair framework that basically follows the classical repair approach, but instead of removing one axiom i from each justification Ji, it replaces i by a weaker axiom i such that (Ji nf ig)[f ig no longer has the unintended consequence. Here we call an axiom weaker than an axiom if logically implies . Our first important result is that, in general, the gentle repair approach needs to be iterated, i.e., applying it once does not necessarily remove the consequence. Our second result is that at most exponentially many iterations (in the number of axioms in the refutable part of O) are always sufficient to reach a repair. 3. The question then is how to come up with appropriate weaker axioms i within the gentle repair framework. To make the repair as gentle as possible, these weakenings should be maximally strong. Instead of allowing for arbitrary ways of weakening axioms, we introduce the notion of a weakening relation, which restricts the way in which axioms can be weakened. We show that, under certain restrictions on this relation (well-founded, one-step generated, effectively finitely branching), maximally strong weakenings w.r.t. it can effectively be computed. 4. The paper then investigates weakening relations on GCIs for the DL EL.
In general, such relations need not be well-behaved. For example, we show that the largest such relation g (which is induced by logical consequence without additional restrictions) is not one-step generated, i.e., the transitive closure of the one-step relation g1 induce by g is strictly contained in g, where the induced one-step relation is defined as g1:= f( ; ) 2 g j there is no such that g g: 5. To obtain weakening relations that have our desired properties (see item 3), we then concentrate on weakening relations on EL GCIs that are obtained by generalizing the right-hand sides of the GCIs. In the semantic weakening relation sub , “generalizing” basically means that the right-hand side of the weaker axiom strictly subsumes the right-hand side of the stronger one. We can show that the relation sub is well-founded, one-step generated, and effectively finitely branching. Thus, maximally strong weakenings w.r.t.
sub can effectively be computed. However, the algorithm obtained from the general result mentioned in item 3 yields a non-elementary upper bound for sub , and the strongest lower bound we are currently able to show is only exponential. 6. To obtain a weakening relation that has better algorithmic properties, we introduce the syntactic weakening relation syn , where a more general righthand side is obtained by removing occurrences of subconcepts from the original one. This relation is also one-step generated, but the other two properties are strengthened to linear branching and to linearly bounded length of syn -chains. For this relation, a single maximally strong weakening can be computed in polynomial time, and all of them can be computed in exponential time. In addition, there may be exponentially many maximally strong weakenings, which shows that the exponential upper bound is optimal.