In the beginning of the Semantic Web, ontologies were usually constructed once by a single knowledge engineer and then used as a static conceptualization of some domain. Nowadays, knowledge bases are increasingly dynamically evolving and incorporate new knowledge from di erent heterogeneous domains { some of which is even contributed by casual users (i.e., non-knowledge engineers) or even software agents. Given that ontologies are based on the rather strict formalism of Description Logics and their inference procedures, con icts are likely to occur during ontology evolution. Con icts, in turn, may cause an ontological knowledge base to become inconsistent and making reasoning impossible. Hence, every formalism for ontology evolution should provide a mechanism for resolving con icts. In this paper we provide a general framework for con ict-free ontology evolution without changing the knowledge representation. Using a variant of Lehmann's Default Logics and Probabilistic Description Logics, we can invalidate unwanted implicit inferences without removing explicitly stated axioms. We show that this method outperforms classical ontology repair w.r.t. the amount of information lost while allowing for automatic con ict-solving when evolving ontologies.
Knowledge in the Semantic Web is represented by ontologies expressed in the Web Ontology Language OWL. The current standard, OWL2 [1], de nes di erent pro les all of which have some Description Logics as a rough syntactic variant, allowing for di erent levels of expressivity. These Description Logics (DL) are decidable fragments of rst-order logics where explicit knowledge is expressed in axioms and assertions. DL knowledge bases have well-de ned model-theoretic semantics that allows to infer new conclusions from existing knowledge.
When ontologies evolve, knowledge is removed or new knowledge is added. By adding new axioms and/or new assertions, contradictions may be introduced that cause the knowledge base as a whole to be inconsistent. For example, adding disjoint-axioms may make some concepts in the ontology unsatis able. When there exists an assertion of some individual to that concept, the knowledge base is inferred to be inconsistent. Yet, for an inconsistent knowledge base any conclusion|even meaningless ones|becomes trivially true. For ontology evolution, it is hence desirable to prevent concepts from being inferred unsatis able. There indeed exist more reasons for why a knowledge base can become inconsistent, but we propose to start o with con ict-free conceptualizations and present a method that never infers any concept to be unsatis able.
Contradictions may be caused by agents that automatically assemble new information from di erent heterogeneous sources. This is likely to happen when combining di erent ontologies, modeled by di erent agents. But even ontologies created by knowledge engineers may contain con icting pieces of knowledge. As such, any framework for ontology evolution has to provide a way for resolving con icts|usually referred to as ontology repair.
Agents querying (or interacting with) an ontology in the Semantic Web assume that both the query and the answer are expressible in OWL2. Furthermore, the answer should have meaningful semantics and should not contain con icts. We therefore propose to demand, in the context of ontology evolution, any formalism for ontology repair to ful ll the following properties: 1. The formalism for knowledge representation is not changed. 2. No concept is inferred unsatis able4. 3. The procedure shall work automatically. 4. The original information should be kept. 5. As little inferred information as possible shall be lost.
Instead of removing axioms (i.e. explicit knowledge), we propose to invalidate those inferences (i.e. implicit knowledge) that cause concepts to be inferred unsatis able. We can show that we lose fewer inferences than in the case of axiom removal. To invalidate only inferences we keep the formalism for knowledge representation. Namely, we consider DL knowledge bases so that the rst desired property is satis ed, and apply the following reasoning approach.
Based on Lehmann's Default Logics [2] and Probabilistic Description Logics [3] our approach separates axioms responsible for a con ict into di erent partitions and collects axioms not involved in a con ict in its separate set. Due to the separate treatment of con ict-causing axioms, inferences for unsatis able concepts are invalidated but the formalism for knowledge representation remains unchanged. To limit the number of inferences lost when reasoning the single partitions are considered alongside with the set of non-con ict axioms. We call the pair of the partition and the set of non-con icting axioms a Default TBox which contains all axioms that occurred in the original ontology. 4 For the current work we concentrate on resolving unsatis able concepts. The procedure may, in principle, be extended to resolve unsatis able roles and|to a certain extent|assertions.
While this method, unfortunately, cannot prevent that some potentially interesting inferences are lost, it limits the loss to a minimum. It can, furthermore, be shown that fewer inferences are lost than in the case of axiom removal|while still working fully automatically. We indeed accept potential modeling errors in the knowledge base, because there is no evidence that tells us how to solve them otherwise.
This work is structured as follows: We start with an overview over OWL, Description Logics and justi cations in Section 2. In the subsequent Section 3 we introduce Default TBoxes and continue in Section 4 with the description of our partition method for invalidating inferences. There we show that the Default TBox resulting from the partition method is consistent and how it can be computed e ciently. We provide experimental results in Section 5 and discuss the ndings of our work in Section 6|followed by an overview over related work in the following Section 7. In the nal Section 8 we conclude the paper and give an outlook on future work. 2
Description Logics (DL) are languages for knowledge representation with a wellde ned syntax and semantics. A DL allows to specify concepts (also known as classes), instances thereof, also referred to as individuals and binary relations, called roles between individuals. Operators such as negation (:) or conjunction (u) enable the construction of complex concepts and roles.
A DL allows to de ne a terminology of concepts. Such a terminology, called a TBox, is a nite set of axioms describing a hierarchy on a set of concepts. TBox axioms are of the form Birds v Animals and express, for example, that the concept Birds is a specialization (or subsumed by) of the concept of Animals. The semantics of these subclass-axioms requires each instance of the concept of Birds also to be an instance of the concept of Animals.
Depending on its expressivity, a DL may also be used for de ning a role hierarchy, called RBox. A nite collection of assertions about individuals is called an ABox. A DL knowledge base is de ned by the triple K = (T; R; A) where T is a TBox, R is an RBox and A is an ABox|each of which is nite and possibly empty.
Interpretations and Satis ability The formal semantics of a DL is given by an interpretation I = ( I ; I ). It consists of the interpretation domain I , a non-empty set, and the interpretation function I which assigns to every atomic concept A a set AI I and to every atomic role R a set RI I I .
In order to nd out whether there exist contradictions in a DL knowledge base K, we have to nd out whether there exists an interpretation that satis es K. An interpretation I is said to satisfy a concept A or a role R, if the result of the interpretation function is not empty. We denote this by I j= A, if AI 6= ; and I j= R, if RI 6= ;, respectively. Concepts that have an empty interpretation are called unsatis able, referred to as T j= U v ?.
For concept subsumption and role inclusion, satis ability is de ned w.r.t. set inclusion. An interpretation I is said to satisfy an inclusion axiom I j= B v A, if BI AI . A TBox T is said to be satis able, if there exists an interpretation I such that I satis es every axiom in T . In this case, we say that I is a model of T . The same holds for RBoxes. In the following, we always assume the RBox to be satis able. 2.1
A DL knowledge representation system (KRS) de nes algorithms to infer implicit knowledge from explicitly stated knowledge. Using these algorithms, a KRS usually supports the following four standard reasoning tasks: Subsumption Test, Satis ability Test, Consistency Test, and Instance Retrieval.
We say that a TBox T entails an axiom , or T j= , if all models of T satisfy . If is a new axiom, i.e. 62 T , we call an inferred axiom. The deductive closure (or extension) of a TBox T is the set of all non-trivial explicitly stated as well as inferred entailments: (T )+ = f j T j= g. Excluding trivial entailments, e.g. C v A u A; C v A t B, we ensure the deductive closure to be nite. We de ne the deductive closure of an RBox in the same way as for TBoxes. 2.2
Knowledge in the Semantic Web is represented by ontologies which are expressed in the Web Ontology Language (OWL). The current standard OWL2 [1] was designed in a way such that it has the DL SROIQ as a rough syntactic variant. SROIQ is a very expressive language, and its reasoning procedures are of high computational complexity. Yet, this expressiveness is not needed in every case. As a consequence, so-called pro les were de ned for OWL2, each of which correspond to a unique DL. Hence, every OWL2 pro le has a well-de ned semantics and a decidable reasoning procedure. The pro les were de ned in a way such that the knowledge representation is unchanged but language constructors are restricted in a way such that the corresponding DL is less expressive.
Thanks to the general nature of the method proposed in this paper we may consider any DL for which there exists a decidable reasoning procedure. In other words: we are not dependent on the expressiveness of the OWL2 pro le used. 2.3
To invalidate an unwanted inference T j= , i.e. removing from (T )+ , we must rst nd out, which axioms are responsible for this very inference. We are hence looking for the minimal sets of axioms J T for which J j= holds [4]. Minimality guarantees that the entailment is invalidated when at least one of the axioms from the corresponding minimal set is not considered alongside with the others in the T when drawing inferences. Justi cations are minimal sets of axioms from a TBox such that an inference still holds: De nition 1. Let T be a TBox. A justi cation for an entailment T j= set of axioms JT ; T such that JT ; j= and J 0 6j= for every J 0 JT ; .
In order to be able to distinguish individual justi cations, we number them by k = 0; : : : ; K where K is the number of justi cations. Consequently, refer to the k-th justi cation by JTk ; .
Justi cations for unsatis able concepts, called unsat justi cations, are of the form JT ;Uv? where U is a (possibly complex) unsatis able concept. Unsat justications may depend completely on the satis ability of other concepts, i.e. they are supersets of other justi cations. If an unsat justi cation does not depend on another one, then we call it a root unsat justi cation.
De nition 2. Let T be a TBox. A justi cation for JT ;Uv? is called a derived unsat justi cation, if there exists some concept U 0 for which JT ;Uv? JT ;U0v?. Otherwise JT ;Uv? is called a root unsat justi cation.
By invalidating some unsat justi cation JT ;Uv?, i.e. by performing some operation such that JT ;Uv? 6j= U v ?, all dependent unsat justi cations are invalidated as well. Hence, invalidating all root unsat justi cations for unsatis able concepts will make every so far unsatis able concept satis able again. Referring to the properties we proposed in Section 1, a framework for con ictfree ontology evolution has to provide a method for automatically invalidating all root unsat justi cations for unsatis able concepts.
JT ;Dv? = JT ;Cv? [ fD whereas JT ;Dv? is derived.
Example 1. Given the simple TBox T = fB v A; C v B; C v : A; D v Cg it is possible to infer the concept C to be unsatis able. The only justi cation for T j= U v ? is JT ;Cv? = fB v A; C v B; C v : Ag. The concept D is also inferred to be unsatis able, but with the justi cation v Cg. As such, JT ;Cv? is a root unsat justi cation 3
In this Section, we de ne a general operator for invalidating inferences. After introducing the formal basics that underly our method for solving con icts we show how it can be applied to the general operator. 3.1
Let T be a TBox and 2 (T )+. Applying some operator ( ) to T , we say the inference T j= is invalidated, if is not contained in the the deductive closure of the result of T , i.e. ( 62 ( T )+). As stated in Section 1, we require the knowledge representation to be unchanged, resulting the deductive closure ( T )+ to be a set of DL axioms as well.
There exist various ways of de ning the (:) operator, like para-consistent logics [5], and removing axioms from T that justify T j= . The latter is the currently most common way for solving con icts and usually referred to as ontology repair. Instead of actually removing an explicitly stated axiom, we propose to split up the TBox such that groups of axioms causing unsatis ability are not used at the same time when drawing inferences. That way it is still possible to reason, even if the KB is unsatis able. We keep the formalism for knowledge representation but have to slightly change the way of inferencing. In order to do this the notion of Default Knowledge Bases is introduced in the following. 3.2
Inference services like Lehmann's Lexicographical Entailment for Default Logics [2] provide exactly the desired properties from Section 1. To achieve these we split the set of axioms into a TBox T and partitions such that for each partition all concepts of all axioms in the partition together with the axioms in T are satis able. We achieve a family of TBoxes (T [ Un)nN=0 which we call a Default TBox. Inferences are invalidated by treating the partitions of axioms separately. De nition 3. Let T and U0; : : : ; UN be mutually disjoint TBoxes. A Default TBox DT is the family of TBoxes DT = (T [ U0; : : : ; T [ UN ).
A Default TBox implies a partitioning on a TBox: T = T U0 : : : UN . According to [2] and [3], a single partition Un is de ned as the set of all axioms B v A in T n (T Snm=10 Um) for which T Snm=10 Um j= A u B. As a result, T [ Un does not infer any concept to be unsatis able. This enables us to de ne a -operator such that the partitioning of a TBox is transformed into a Default TBox: De nition 4. Let T be a TBox and U0; : : : ; UNSNbe a family of disjoint subsets of T . Let further be Tn = T [ Un, and T = T n n=0 Un. The Default -operator transforms T and U0; : : : ; UN to a Default TBox:
T (U0; : : : ; UN ) = DT with DT = (Tn)nN=1 3.3
A Default TBox is a wrapper for a set of classical TBoxes. Hence, inference services like checking axiom satis ability and consistency can be applied by means of the inference service de ned for the original TBox. Consequently, we introduce the following de nitions:
A Default TBox DT is said to entail an axiom, DT j= , if one of its TBoxes entails . As a result, the deductive closure of a Default TBox is de ned by (DT )+ = SnN=0(Tn)+. We say that DT is satis able if all of its TBoxes are satis able.
Please note that this inference service for a Default TBox is not the same inference service as de ned by Lehmann's Lexicographical Entailment: We borrowed the method of how to separate axioms from each other into partitions but we compute regular models instead of lex-minimal models. The actual partitioning process is described in Section 4. As we consider axioms separately during reasoning, we will lose inferences. In the sequel, we show which inferences are actually lost by separating axioms into di erent partitions.
Compared to the original TBox, in the Default TBox all inferences whose justi cations share axioms that are contained in di erent partitions are invalidated: (T )+ n (DT )+ = f j JT ; \ Un 6= ; ^
JT ; \ Um 6= ; ^ n 6= mg In Example 1, a valid Default TBox was T = fD v Cg and U0 = fB v Ag and U1 = fC v B; C v : Ag. While the bad inferences C v ? and D v ? are invalidated, also C v A and D v A are not valid anymore. On the other hand, for the Default TBox T = fC v B; D v Cg and U0 = fB v Ag and U1 = fC v : Ag these inferences are preserved.
If we applied classical ontology repair, i.e. axiom removal, not only we delete the removed axioms from the deductive closure of the TBox, but even inferences whose justi cations contain just one of the removed axiom are invalidated|in contrast to our method where we only invalidate justi cations containing pairs of axioms that are in di erent partitions. We hence claim that using our method for de ning the -operator, it can be expected that fewer inferences are invalidated. 4
To resolve unsatis able concepts, we split up the sets of trouble-causing axioms, i.e. the root justi cations for unsatis able concepts, into di erent partitions. This is achieved by applying the adapted version of the partition method from Lehmann's Lexicographical Entailment [2] as de ned for Probabilistic Description Logics [3] that we introduced in [6].
In [6] we showed that under certain conditions we can compute a valid partition consisting of all the axioms of the root unsat justi cations without additional satis ability checks. This methods indeed de nes a -operator for invalidating all troublesome inferences T j= U v ?. We here show that we can improve this -operator by putting only exactly two axioms of each root unsat justi cation into the partitions whereas the remaining axioms can be put in the TBox. Fewer axioms in the partitions, in turn, means potentially loosing fewer inferences.
We will not change the working principle of the procedure introduced in [6]. As a result, the improved procedure will also be a valid -operator. In the following we show how the splitting can be used for computing the partitions. We show by induction which axioms of the root justi cations we have to chose for the partitions Unof the Default TBox and which we may leave for T . We split-up any unsat justi cation JTk ;Uv? into the splitting sets [6]: k k Uv? = fU v A 2 JT ;Uv?g and
Uk = JT ;Uv? n U k k
We refer to axioms from the rst as -axioms whereas we call axiom from the latter -axioms.
Example 2. For the TBox T = <8 ((41)) DB v B u :8AR:fpg ((52)) 9RE:> vv :AD
: (
=
(
Algorithm 1 describes the improved procedure for nding partitions from the
splitting. In the sequel we will illustrate its working principles by Example 2.
Initializing T For all axioms B v A that do not occur in any root justi
cation, the requirement A u B to be satis able is trivially ful lled. Hence, we
initialize T with T = T n SkK JTk ;Uv?. In Example 2, the only axioms that
are not part of any root justi cation are (
Computing a Partition For computing a partition, we consider all those root justi cations for which neither of their -axioms occurs in a -set of any other unsat justi cation (Line 15).
In Example 2, axioms (
We resolved D1v?, and remove it from the splitting sets (Line 18). We take
exactly one axiom from its -set and add it to partition U1 (Line 6). In this
case, D1 v? = f(
JTk ;Uv?g f Uv?gkK=1;
k 17: 18: 19: end for 20: n n + 1 21: end while f Ukv?gkK=1; n
0 -sets whose
-set was removed
JTk ;Uv?g k n Uv? end for // Resolve -sets having axioms not contained in any for all Ukv? with Ukv? n SkK0=0 Uk00v? 6= ; do
Un Un [ f g for exactly one 2 Ukv? n SkK0=0 Uk00v? T T [ Ukv? n (Un [ SkK0=0 Uk00v?) // remove solved -sets. -set Algorithm 1 The partitioning algorithm.
Input: 1. TBox T , 2. Split-up unsat justi cations J = fJTk ;Uv?g for k = 0; : : : ; K Output:
Default TBox DT = (T [ U0; : : : ; T [ UN ) justi cation JT1 ;Dv?, as well as the dependent unsat justi cations JT3 ;F v? and JT4 ;HuJv?, all of whose splitting sets we remove (Lines 10, 12).
Axiom (
We again resolve its corresponding -set which contains only axiom (
When the procedure terminates, all dependent unsat justi cations have been resolved, i.e. the Default TBox DT = T (U0; : : : ; UN ) does not infer any of its concepts to be unsatis able. Since the partitions Un were constructed according to [3], for any choice of the -axioms, DT is consistent. Note that the actual number of partitions and their axioms depend on the choice of -axioms, but are unique for each choice. This also means that each choice may invalidate di erent sets of inferred entailments and, as a result, the impact of the Default -operator depends on the actual choice made.
In Example 2, the Default TBox is determined by T = f(
To evaluate the presented approach, we performed experiments on three
ontologies that are known to contain unsatis able concepts. We compared the
deductive closure of the original TBox with (
If an ontology contains an unsatis able concept, depending on the reasoner, the concept hierarchy for unsatis able concepts might be unde ned. Hence, we compute an approximation of the deductive closure of the original TBox (containing unsatis able concepts) as the union of the deductive closures of all TBoxes Tr that result from all possible repair solutions. For comparison, we took the repair solution where the minimal number of inferences is lost.
We computed the deductive closure for each of the possible Default TBoxes that can be obtained using the presented approach. For comparison with deductive closure of the original TBox and the best repair solution, we took that Default TBox solution DT sgl where the minimal number of inferences is lost.
Furthermore, we computed the deductive closure for the Default TBox DT all where we put all axioms from all root unsat justi cations into partitions. Since its solution is unique, we can use it directly for comparison with the deductive closure of the original TBox and the best repair solution.
For computing justi cations we used the black-box approach described in [7]. All experiments were performed using the Pellet OWL2 reasoner [8], version 2.2.0, and the Manchester OWL API [9], version 3.0.
j(T )+j j(Tr)+j
Koala Chemical
Pizza As can be seen from Table 1, the deductive closure of the best solution of our approach DT sgl (column 4) is, for all ontologies we tested, larger than the deductive closure of the best solution for axiom removal Tr (column 2). This, in turn, means that the number of entailments invalidated is always lower comparing the best solution of our approach with the best solution of removing axioms. Furthermore, we outperform axiom removal in the sense that the best solution of axiom removal does not preserve any inference di erent from our approach (column 6).
However, this is not true for the original version of our approach. If we put all axioms of all root unsat justi cations into the partitions of the Default TBox DT all (column 3), we invalidate more inferences than than both the improved version and even the best solution of axiom removal do. However, the actual inferences invalidated di er for the original approach and the best removal solution (column 5). For the Koala and the Pizza ontology the di erence is caused by the fact that, w.r.t. the original TBox T , axioms were actually removed from Tr but not from DT all. In contrast to that, the set of inferences invalidated di ers in more than the removed axioms for the more complex Chemical ontology. 6
The experimental results support our claim that using our approach we can nd a solution which invalidates fewer inferences than using classical axiom removal for ontology repair. We, furthermore, showed that the presented more ne-grained approach indeed improves its original version.
Neither axiom removal nor our approach make a deterministic choice w.r.t. any performance measure that takes into account the number of inferences a choice invalidates. On the one hand, computing all possible solutions is not feasible for large ontologies, on the other hand, the computation of a single valid solution is cheap. Hence, optimization strategies like a stochastic search seem promising for nding optimal solutions.
Our approach is restricted to solving con icts for unsatis able concepts. In an OWL2 knowledge base, however, roles may become unsatis able and inconsistencies (i.e. assertions that cause the ABox not to be a model of the TBox) may occur. Since OWL2, the treatment of roles has become similar to the treatment of concepts. Hence, the approach of splitting sets of axioms that support a role con ict in the TBox may also be applied to unsatis able roles. To address inconsistencies we may use abduction to add a new concept for assertions causing an inconsistency. Alternatively, we could treat instances like concepts and apply our approach directly.
We only tested our approach on a few rather small knowledge bases. The complexity of the whole procedure we presented is dominated by the computation of all root justi cations for all unsatis able concepts. However, when we evolve a knowledge base, incremental reasoning [10] may signi cantly reduce the computation time. If there was a way how to maintain the root unsat justi cations for a TBox, our procedure, and ontology-repair in general, computing all root unsat justi cations becomes feasible even for large Semantic Web knowledge bases. 7
In recent years, much progress has been made in the task to explain why a conclusion can be drawn from a DL knowledge base by solely using axioms from the knowledge base itself. Schlobach and Cornet [4] came up with minimal unsatis able preserving sub-TBoxes (MUPS) which can explain the reason for unsatis ability of concepts. Kalyanpur et al. [11] introduced justi cation as a form of minimal explanation for any arbitrary entailment. It could be shown that computing all justi cations for an entailment is feasible in the tableaux calculus [11]. Recent approaches try to compute ne-grained [12] or laconic justi cations [13] to consider only the con ict causing sub-parts of an axiom.
In the area of con ict-free ontology evolution, the main focus usually lies on resolving inconsistencies and hence changes mainly occur on instance level or rather restricted TBoxes [14]. Repair can also be done using higher-order logics like in the Ontology Repair System [15]. This, however, makes changes to the knowledge representation and cannot be applied to OWL ontologies in a straightforward way.
Alternatives to do reasoning with incoherent DL knowledge bases are, for example, para-consistent logics [5]. However, these change the notion of inference and hence their semantics much more than default logic does.
Default Logics were rst introduced by Reiter [16]. Because of undecidability issues Lehmann provided a simpler perspective on Default Logics [2] introducing the concept of partitions. Lukasiewicz extended this approach by a separate TBox that contains all the axioms which still model crisp and not default knowledge [3]. He also enriched defaults by belief intervals resulting in a probabilistic variant of the DL SHOIN (D) referred to as P SHOIN (D) or Probabilistic Description Logics. While in this paper we make use of the partition approach enriched by a TBox, we do not consider the possibility of assigning the axioms belief intervals|although this should, in principle, be possible.
There have been made propositions of how to incorporate default knowledge in OWL-DL knowledge bases in [17] [18], and [19]. While the rst two deal with applications of Reiter's interpretation of defaults, to our knowledge, P-SHOIN (D) [3] is currently the only formalism providing default reasoning services w.r.t. Lehmann's lexicographical entailment for OWL DL knowledge bases for which an implementation is available [20]. 8
In this paper, we presented an approach for automatic con ict-free ontology evolution. We de ned a general framework and proposed a variant of Lehmann's Default Logics and Probabilistic Description Logics that relies upon the idea of considering con ict-causing axioms separately when drawing inferences. In contrast to classical ontology repair, we proposed to keep the explicitly stated axioms but remove only implicit inferences for solving con icts. This separation can be achieved by applying a splitting scheme to the root justi cations for con icts, which are, in our case, unsatis able concepts. The partition and the remaining axioms form a Default TBox, which slightly changes the inferencing procedure but leaves the knowledge representation untouched. The deductive closure of the automatically constructed Default TBox was shown to be free of con icts. Experimental results con rmed that applying our method fewer inferences were lost than in the case of classical automatic ontology repair.
However, we restricted our experiments to rather small knowledge bases compared to what is currently considered as a large knowledge base. The main reason for this limitation is the computational complexity of the generation of justi cations for all unsatis able concepts. If it were possible to e ciently maintain justi cations for evolving knowledge bases, the approach could also be applied to large scale knowledge bases.
The choice of the actual partition for the Default TBox is non-deterministic. For large scale knowledge bases, computing solutions is likely to become unfeasible. Hence, optimization strategies, like a stochastic search process, may be applied to look for an optimal solution. Such optimization strategies may also take into account more sophisticated performance measures like the impact of invalidated inferences instead of just counting their total number.
Since current approaches to the computation of ne-grained justi cations increasingly aim to only address sub-parts of the axioms, future work will investigate how parts of axioms may be used for a Default TBox. Last, we restricted con icts to unsatis able concepts. Since the presented approach is rather generic, it should, in general, be applicable to unsatis able roles and inconsistencies as well.
As sketched above, all these limitations do not invalidate the general approach but are the subject of future work. Indeed we believe that ontology repair using the presented approach has the potential to enable automatic con ict-free ontology evolution in practice|a central need for long living ontologies and, hence, for the Semantic Web.