{'fraction_non_alphanumeric': 0.03952866454955708, 'fraction_numerical': 0.007270600033428046, 'mean_word_length': 4.27728776185226, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 2, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Get my pizza right: Repairing missing is-a relations in ALC ontologies (extended version)

With the increased use of ontologies in semantically-enabled applications, the issue of debugging defects in ontologies has become increasingly important. These defects can lead to wrong or incomplete results for the applications. Debugging consists of the phases of detection and repairing. In this paper we focus on the repairing phase of a particular kind of defects, i.e. the missing relations in the is-a hierarchy. Previous work has dealt with the case of taxonomies. In this work we extend the scope to deal with ALC ontologies that can be represented using acyclic terminologies. We present algorithms and discuss a system.


Introduction
Developing ontologies is not an easy task, and often the resulting ontologies are not consistent or complete. Such ontologies, although often useful, also lead to problems when used in semantically-enabled applications. Wrong conclusions may be derived or valid conclusions may be missed. Defects in ontologies can take different forms (e.g. [16]). Syntactic defects are usually easy to find and to resolve. Defects regarding style include such things as unintended redundancy. More interesting and severe defects are the modeling defects which require domain knowledge to detect and resolve, and semantic defects such as unsatisfiable concepts and inconsistent ontologies. Most work up to date has focused on debugging (i.e. detecting and repairing) the semantic defects in an ontology (e.g. [16,15,29,5]). Modeling defects have mainly been discussed in [2,20,19] for taxonomies, i.e. from a knowledge representation point of view, a simple kind of ontologies. The focus has been on defects regarding the is-a structure of the taxonomies. In this paper we tackle the problem of repairing the is-a structure of ALC ontologies that can be represented using acyclic terminologies.
In addition to its importance for the correct modeling of a domain, the structural information in ontologies is also important in semantically-enabled applications. For instance, the is-a structure is used in ontology-based search and annotation. In ontology-based search, queries are refined and expanded by moving up and down the hierarchy of concepts. Incomplete structure in ontologies influences the quality of the search results. As an example, suppose we want to find articles in the MeSH (Medical Subject Headings [25], controlled vocabulary of the National Library of Medicine, US) Database of PubMed [27] using the term Scleral Diseases in MeSH. By default the query will follow the hierarchy of MeSH and include more specific terms for searching, such as Scleritis. If the relation between Scleral Diseases and Scleritis is missing in MeSH, we will miss 738 articles in the search result, which is about 55% of the original result. The structural information is also important information in ontology engineering research. For instance, most current ontology alignment systems use structurebased strategies to find mappings between the terms in different ontologies (e.g. overview in [21]) and the modeling defects in the structure of the ontologies have an important influence on the quality of the ontology alignment results.
Debugging modeling defects in ontologies consists of two phases, detection and repair. There are different ways to detect missing is-a relations. One way is by inspection of the ontologies by domain experts. Another way is to use external knowledge sources. For instance, there is much work on finding relationships between terms in the ontology learning area [3]. In this setting, new ontology elements are derived from text using knowledge acquisition techniques. Regarding the detection of is-a relations, one paradigm is based on linguistics using lexico-syntactic patterns. The pioneering research conducted in this line is in [11], which defines a set of patterns indicating is-a relationships between words in the text. Another paradigm is based on machine learning and statistical methods. Further, guidelines based on logical patterns can be used [5]. When the ontology is part of a network of ontologies connected by mappings between the ontologies, knowledge inherent in the ontology network can be used to detect missing is-a relations using logical derivation [2,20,19]. However, although there are many approaches to detect missing is-a relations, these approaches, in general, do not detect all missing is-a relations. For instance, although the precision for the linguistics-based approaches is high, their recall is usually very low.
In this paper we assume that the detection phase has been performed. We assume that we have obtained a set of missing is-a relations for a given ontology and focus on the repairing phase. In the case where our set of missing is-a relations contains all missing is-a relations, the repairing phase is easy. We just add all missing is-a relations to the ontology and a reasoner can compute all logical consequences. However, when the set of missing is-a relations does not contain all missing is-a relations -and this is the common case -there are different ways to repair the ontology. The easiest way is still to just add the missing is-a relations to the ontology. For instance, Figure 1 shows a small part of a pizza ontology based on [26], that is relevant for our discussions. Assume that we have detected that MyPizza⊑ FishyMeatyPizza and MyFruttiDiMare ⊑ NonVegetarianPizza are missing is-a relations. Obviously, adding MyPizza⊑ FishyMeatyPizza and MyFruttiDiMare⊑ NonVegetarianPizza to the ontology will repair the missing is-a structure. However, there are other more interesting possibilities. For instance, adding AnchoviesTopping⊑ FishTopping and ParmaHamTopping⊑ MeatTopping will also repair the missing is-a structure. Another more informative way 1 to repair the missing is-a structure is to add AnchoviesTopping⊑ FishTopping and ParmaHamTopping⊑ HamTopping. Essentially, these other possibilities to repair the ontology include missing is-a relations (e.g. AnchoviesTopping⊑ FishTopping) that were not originally detected by the detection algorithm. 2 We also note that from a logical point of view, adding AnchoviesTopping⊑ MeatTopping and ParmaHamTopping⊑ FishTopping also repairs the missing is-a structure. However, from the point of view of the domain, this solution is not correct. Therefore, as it is the case for all approaches for debugging modeling defects, a domain expert needs to validate the logical solutions.
The contributions of this paper are threefold. First, we show that the problem of finding possible ways to repair the missing is-a structure in an ontology in general can be formalized as a generalized version of the TBox abduction problem (Section 3). Second, we propose an algorithm to generate different ways to repair the missing is-a structure in ALC ontologies that can be represented using acyclic terminologies (Section 4). Third, we discuss a system that allows a domain expert to repair the missing is-a structure in Section 5. We discuss the functionality and user interface of the repairing system and show an example run. Further, we discuss related work in Section 6 and conclude in Section 7. We continue, however, with some necessary preliminaries in Section 2.

Preliminaries
In this paper we deal with ontologies represented in the description logic ALC with acyclic terminologies (e.g. [1]). Concept descriptions are defined using constructors as well as concept and role names. As constructors ALC allows concept conjunction (C ⊓ D), disjunction (C ⊔ D), negation (¬ C), universal quantification (∀ r.C) and existential quantification (∃ r.C). 3 In this paper we consider ontologies that can be represented by a TBox that is an acyclic terminology. An acyclic terminology is a finite set of concept definitions (i.e. terminological axioms of the form C . = D where C is a concept name) that neither contains multiple definitions nor cyclic definitions. 4 An ABox contains assertional 1 This is more informative in the sense that the former is derivable from the latter.
Adding ParmaHamTopping⊑ HamTopping, also allows to derive ParmaHamTop-ping⊑ MeatTopping as the ontology already includes HamTopping⊑ MeatTopping. 2 Therefore, the approach discussed in this paper can also be seen as a detection method that takes already found missing is-a relations as input. 3 C and D represent concepts, and r represents a role. 4 We observe that the TBox in Figure 1 is not an acyclic terminology as there are statements of the form A⊑ C. However, it is possible to create an equivalent TBox knowledge, i.e. statements about the membership of individuals (interpreted as elements in the domain) to concepts (C(i)) as well as relations between individuals (r(i,j)). 5 A knowledge base contains a TBox and an ABox. A model of the TBox/ABox/knowledge base satisfies all axioms of the TBox/ABox/knowledge base. A knowledge base is consistent if it does not contain contradictions. An important reasoning service is the checking of (un)satisfilibility of concepts (a concept is unsatisfiable if it is necessarily interpreted as the empty set in all models of the TBox/ABox/knowledge base, satisfiable otherwise). A TBox is incoherent if it contains an unsatisfiable concept.
Checking satisfiability of concepts in ALC can be done using a tableau-based algorithm (e.g. [1]). To test whether a concept C is satisfiable such an algorithm that is a acyclic terminology by replacing the statements of the form A⊑ C with A . = C ⊓ A where A is new atomic concept. See Figure 2. 5 i and j represent individuals. In the completion graph in Section 4 statements of the form C(i) are written as i : C, and statements of the form r(i,j) are written as irj.
⊓-rule: if the ABox contains (C1 ⊓ C2)(x), but it does not contain both C1(x) and C2(x), then these are added to the ABox. ⊔-rule: if the ABox contains (C1 ⊔ C2)(x), but it contains neither C1(x) nor C2(x), then two ABoxes are created representing the two choices of adding C1(x) or adding C2(x). ∀-rule: if the ABox contains (∀ r.C)(x) and r(x,y), but it does not contain C(y), then this is added to the ABox. ∃-rule: if the ABox contains (∃ r.C)(x) but there is no individual z such that r(x,z) and C(z) are in the ABox, then r(x,y) and C(y) with y an individual name not occurring in the ABox, are added. starts with an ABox containing the statement C(x) where x is a new individual and it is usually assumed that C is normalized to negation normal form. It then applies consistency-preserving transformation rules to the ABox ( Figure 3). The ⊓-, ∀and ∃-rules extend the ABox while the ⊔-rule creates multiple ABoxes. The algorithm continues applying these transformation rules to the ABoxes until no more rules apply. This process is called completion and if one of the final ABoxes does not contain a contradiction (we say that it is open), then satisfiability is proven, otherwise unsatisfiability is proven. One way of implementing this approach is through completion graphs which are directed graphs in which every node represents an ABox. Application of the ⊔-rule produces new nodes with one statement each, while the other rules add statements to the node on which the rule is applied. The ABox for a node contains all the statements of the node as well as the statements of the nodes on the path to the root. Satisfiability is proven if at least one of the ABoxes connected to a leaf node does not contain a contradiction, otherwise unsatisfiability is proven.
In this paper we assume that an ontology O is represented by a knowledge base containing a TBox that is an acyclic terminology and an empty ABox. In this case reasoning can be reduced to reasoning without the TBox by unfolding the definitions. However, for efficiency reasons, instead of running the previously described satisfiability checking algorithm on an unfolded concept description, the unfolding is usually performed on demand within the satisifiability checking algorithm. It has been proven that satisfiability checking w.r.t. acyclic terminologies is PSPACE-complete in ALC [23].

An abduction problem
In our setting, a missing is-a relation in an ontology O represented by a knowledge base KB, is an is-a relation between named concepts that is not derivable from the KB, but that is correct according to the intended domain. We assume that we have a set M of missing is-a relations (but not necessarily all) for O. Then, the is-a structure of O can be repaired by adding is-a relations (or axioms of the form C⊑ D) between named concepts to O such that the missing is-a relations can be derived from the repaired ontology. This repair problem can be formulated as a generalized version of the TBox abduction problem.
In our setting the language L is ALC and L ′ only allows named concepts. We say that any solution in S GT (KB, {(C i , D i )} i ) is a repairing action. A repairing action is thus a set of is-a relations. When m = 1, this definition of the generalized TBox abduction problem coincides with the TBox abduction problem as formulated in [8], which therefore deals with repairing one missing is-a relation. 6 This shows that solving a generalized TBox abduction problem can be done by solving m TBox abduction problems and then taking the intersection of the solutions. In practice, however, this leads to a number of difficulties. First, it would mean that a domain expert will need to choose between large sets of repairing actions for all the missing is-a relations at once, and this may be a very hard task. Further, due to the size of the solution space, even generating all solutions for one TBox abduction problem is, in general, infeasible. Also, many of the solutions will not be interesting for a domain expert (e.g. [20]). For instance, there may be solutions containing is-a relations that do not contribute to the actual repairing. Some solutions may introduce unintended equivalence relations.
A common way to limit the number of possible solutions is to introduce constraints, e.g. minimality. Our proposed algorithm generates solutions to a TBox abduction problem that are minimal in the sense that repairing actions only contain necessary information for repairing the missing is-a relations. Further, we check the generated solutions for the introduction of incoherence.

Basic algorithm
The basic algorithm for generating repairing actions for a set of given missing is-a relations for an ontology is shown in Figure 4. In this first study we assume that the existing structure in the ontology is correct. Also, as stated in the definition in Section 3, adding the missing is-a relations to the ontology does not lead to incoherence.
In step 1 a set of repairing actions is generated for each missing is-a relation (thereby solving a TBox abduction problem for each missing is-a relation). In 1.1 G = completion graph after running a tableaux algorithm with Ai ⊓ ¬Bi as input on KB; 1.2 Leaf-ABoxes = get ABoxes of the leaves from the completion graph G; 1.
3 For every open ABox A ∈ Leaf-ABoxes: step 1.1 we run the satisfiability checking algorithm with unfolding on demand as described in Section 2, on KB with input A i ⊓ ¬B i , and we collect the ABoxes of the leaves in step 1.2. As A i⊑ B i is a missing is-a relation, it cannot be derived from KB and thus the completion graph will have open leaf ABoxes. We then generate different ways to close these ABoxes in step 1.3. For each individual x in an open leaf ABox we collect the concepts in the statements of the form x:A in P os x and the concepts in the statements of the form x:¬B in N eg x where A and B are named concepts. The ABox can be closed if A⊑ B is added to the ontology for any A ∈ P os x and B ∈ N eg x . Indeed, with this extra information x:A could be unfolded and x:B would be added to the ABox, and this gives a contradiction with x:¬B which was already in the ABox. A repairing action for the missing is-a relation is then a set of A⊑ B that closes each open leaf ABox. In step 1.5 we generate such sets by selecting one such axiom per open leaf ABox and remove redundancy based on the sub-set relation. If a repairing action is a super-set of another repairing action, it is removed. Further, we remove solutions that introduce incoherence.
In step 2 the repairing actions set for all missing is-a relations is initialized with the set of missing is-a relations. Therefore, there will always be at least one repairing action. In step 3 additional repairing actions are generated by combining repairing actions for the individual missing is-a relations. As repairing actions are sets, there are no duplicates in a repairing action. In step 4 we remove redundancy based on the sub-set relation. In step 5 we remove solutions that introduce incoherence. We note that there always will be at least one solution that does not introduce incoherence (i.e. M or a sub-set of M).  As an example, consider the acyclic terminology in Figure 2 equivalent to the ontology in Figure 1 and M = {MyPizza⊑ FishyMeatyPizza, MyFruttiDi-Mare⊑ NonVegetarianPizza}. For the missing is-a relation MyPizza⊑ Fishy-MeatyPizza the completion graph obtained after running the satisfiability check on M yP izza⊓¬F ishyM eatyP izza is shown in Figure 13. The completion graph contains 17 nodes of which 11 are leaf nodes. Of these leaf nodes 6 are closed and the repairing actions will be based on the 5 open leaf nodes. The computation of the P os xj , N eg xj and R A for the leaf ABoxes is given in Figure 14. Closing all open leaf ABoxes will lead to 11 non-redundant repairing actions (see Figure 5) of which 8 lead to incoherence (marked by * in Figure 5). The remaining repairing actions are {MyPizza⊑ FishyMeatyPizza}, {AnchoviesTopping⊑ FishTopping, ParmaHamTopping⊑ MeatTopping } and {ParmaHamTopping⊑ FishTopping, AnchoviesTopping⊑ MeatTopping}. Observe that in this example we removed the repairing actions containing a concept of the form A. This is because whenever x:A occurs in an ABox, then also x:A is in that ABox, as x:A only can appear by unfolding A in x:A. Therefore, whenever A is a choice for repairing, then also A is a choice for repairing, and we can ignore the A choice, which does not relate to a concept in the original ontology.
In a similar way, for missing is-a relation MyFruttiDiMare⊑ NonVegetar-ianPizza, we find the following non-redundant coherence-preserving repairing actions: {MyFruttiDiMare⊑ NonVegetarianPizza}, {AnchoviesTopping⊑ Fish-Topping} and {AnchoviesTopping⊑ MeatTopping}. After combining the repairing actions for the individual missing is-a relations, and removing redundancy and incoherence-introducing repairing actions, we obtain the following 5 solutions for the repairing of the missing is-a structure: A repairing action is a set of statements of the form A⊑ B with A and B named concepts. We note that for acyclic terminologies, after adding such a statement, the resulting TBox is not an acyclic terminology anymore. If this is needed, then instead of adding A⊑ B the following should be done. If there is no definition for A yet in the TBox, then add A .

Solution properties
We prove that the algorithm is correct. In the following A and B are named concepts. Figure 4 contains x:A and x:¬B for some individual x, then adding A ⊑ B to the ontology will close this ABox.

Lemma 1 If an ABox in the algorithm in
Proof. Adding A ⊑ B to an acyclic terminology can be done in the following way. If there is no definition for A yet in the TBox, then add A .
In both cases it will allow an unfolding step in the ABox for x:A such that x:B ⊓ A or x:B ⊓ C is added to the ABox. A further application of the ⊓-rule will then also add x:B to the ABox. This leads to a contradiction with x:¬B and closes the ABox. ♣ Lemma 2 Let G be the completion graph after running the tableaux algorithm with A i ⊓ ¬B i as input on KB. Let G e be the completion graph when running the tableaux algorithm with A i ⊓ ¬B i as input on KB e , the knowledge base for the extended ontology where (i) a statement A .
Proof. We observe that the statements that are valid in the original ontology are still valid in the extended ontology. Also, all transformation rules that could be applied in the tableaux algorithm on the original ontology can also be applied on the extended ontology. Further, additionally, for the extended ontology, there may be an unfolding based on the extension (i.e. when x:A appears in an ABox, then by unfolding x:B (and in case (i) also x:A) should be added), as well as additional applications of transformation rules based on x:B and its consequences. Therefore, assume that A e is an open leaf ABox in G e . Then A e will contain statements that are a result of transformations that could have been peformed in the original ontology as well as statements that can only be derived based on x:B.
A node n tagged with θ changes its tag to σ if: 1. node n has an incoming unf old edge from a σ-tagged node p 2. node n has an incoming ⊓ edge from a σ-tagged node p 3. node n has an incoming ∃i edge from a σ-tagged node p 4. node n has an incoming ∃c edge from a σ-tagged node p 5. node n has an incoming ∀i edge from a σ-tagged node pi and an incoming ∀c edge from a σ-tagged node pc 6. node n has an incoming ⊔ edge from a σ-tagged node p and all other nodes with an incoming ⊔ edge from p are tagged with θ 7. node n has an incoming ⊔ edge from a σ-tagged node p and there are no other nodes with an incoming ⊔ edge from p Fig. 6. Tagging rules.
In order to identify which statements in A e belong to which of these two categories, we built a dependency graph DG = (V, E) where the vertices represent statements from A e , and there is an edge from node n i related to statement τ i to node n j related to statement τ j if τ j could be a direct result of applying some transformation rule or unfolding on τ i . We label the edges with ⊓, ⊔, ∃ i (from a node related to x:∃r.D to a node related to xry), ∃ c (from a node related to x:∃r.D to a node related to y:D), ∀ i (from a node related to xry to a node related to y:C), ∀ c (from a node related to x:∀r.C to a node related to y:C) and unf old depending on which transformation rule was applied.
Further, we tag the nodes in the dependency graph using σ and θ. When the tagging is finished, the statements related to the nodes tagged with σ are a result of transformations that could have been performed in the original ontology. The algorithm for tagging nodes is given in Figure 7. Initially, the node related to x:A i ⊓ ¬B i is tagged with σ. Further, for case (i) all nodes related to z:A and z:B ⊓ A for some individual z are tagged with θ and this tag can never be changed 7 ; All other nodes are initially tagged with θ and collected in the set θ-nodes. We then traverse the dependency graph and change θ tags into σ tags according to a number of rules. Essentially, the tagging simulates the construction of a completion graph (step 4) by first using ⊓, ∀, ∃ and unfolding rules until no more such rules are applicable (essentially an ABox in the completion graph). This is achieved in step 4.1. by applying the tagging rules 1-5 in Figure 6. For case (ii) we need to deal with a special case when unfolding x:A (step 4.1.2). When no more such rules can be applied, but a ⊔-rule could be applied, a choice is made and the procedure is repeated (essentially a child ABox in the completion graph is created and then if needed, further descendant ABoxes). This is achieved by using tagging rules 6 and 7 in Figure 6 in step 4.4.
Step 4 finishes when all nodes have σ tags or no more tagging rules can be applied to nodes with θ tags.
We now show that the set of statements related to σ-tagged nodes is an open leaf ABox A in G (with possible renaming of individuals). It is clear that A ⊆ A e . Further, A contains statements that can be derived by running the tableaux algorithm on the original ontology with A i ⊓ ¬B i as input. (Without Input: The initial dependency graph DG. Output: Tagged dependency graph. Algorithm 1. Tag the node related to x:Ai ⊓ ¬Bi with σ. 1(i). Only for case (i): Tag all nodes related to z:A and z:B ⊓ A for some indivdual z with θ; 2. Tag all remaining nodes with θ and add them to the set θ-nodes; 3. V isited := ∅; 4. While θ-nodes = ∅ and θ-nodes = V isited, do: 4.1 While θ-nodes = ∅ and θ-nodes = V isited, do: 4.1.1 Select a node n ∈ θ-nodes \ V isited and add n to V isited; 4.1.2 If n is related to x:B⊓C for some x and rule 1 is applicable for unfolding a σ-tagged node related to x:A (only case (ii)  loss of generality, individuals may be renamed.) The dependency graph shows which transformation rules and unfoldings can be performed. A is also a leaf ABox in the completion graph obtained by running the tableaux algorithm on the original ontology with A i ⊓ ¬B i as input. If A were not a leaf ABox in that completion graph, then there would be other statements that could be added through the application of the transformation rules or unfolding. However, in that case, these transformation rules or unfoldings could also be applied to A e and these statements could be added to A e , which would contradict the fact that A e is a leaf ABox. Finally, as A ⊆ A e and as A e does not contain a contradiction (as it is an open leaf ABox in G e ), also A does not contain a contradiction. ♣ Consider the example ontology in Figure 8(a) and assume we run the tableaux algorithm with input x:A ⊓ ¬F. The completion graph is given in Figure 9(a). Figure 9(b) shows a completion graph for running the tableaux algorithm with input A ⊓ ¬F on the ontology that extends the original ontology with the axiom A . = B ⊓ A (Figure 8(b)). The completion graph G e contains two open leaf ABoxes, ABox 1.2.1 and ABox 1.2.2. We observe that ABox 1.2.1 in Figure 9  contains all literals from ABox 1.1 in Figure 9(a) and ABox 1.2.2 in Figure 9(b) contains all literals from ABox 1.2 in Figure 9(a). Figure 10(a) shows an initial dependency graph for ABox 1.2.1. In this example all but x:A ⊓¬F can be the direct result of the application of a transformation rule or unfolding of only one other statement. In general this is not case, though. Initially, the node related to (1) is tagged as σ. All other nodes are tagged with θ, and the tag of the nodes related to (3) and (5) cannot be changed. In the first iteration the tags of the nodes related to (2), (9) and (10) will be changed to σ using the tagging rules 1 and 2. Further, the tag for the node related to (14) is changed to σ using tagging rule 7. Then, there will be no more changes in the tagging and the statements related to the nodes with σ tags in Figure 10(b) constitute the statements in ABox 1.1. in Figure 9(a).
The previous lemma also holds when adding sets of axioms of the form (i) A . = B ⊓ A or changing a sets of axioms (ii) of the form A . = C to axioms of the form A .

Lemma 3 Let G be the completion graph after running the tableaux algorithm with
(b) Tagged dependency graph for ABox 1.2.1. in Figure 9(b).  Adding {P 1⊑ N 1 , . . ., P m⊑ N m } to an ontology means adding statements of the form P j . = N j ⊓ P j with P j a new atomic concept or changing statements of the form P j . = C to P j . = N j ⊓ C. Assume G and G e are the completion graphs obtained by running the tableaux algorithm with A i ⊓ ¬B i as input on the knowledge bases of the original (with added missing is-a relations except A i⊑ B i ) and the extended ontology respectively.

Lemma 4 Any element of Rep(A i , B i ) repairs the missing is-a relation
We now prove that every leaf ABox in G e is closed. Let us assume that there exists an open ABox A e in G e . According to the previous lemma, we know then that for A e there is a corresponding leaf ABox A in G such that A ⊆ A e . Further, there is at least one individual x and named concepts P and N such that x:P and x:¬ N are statements in the ABox A 8 . R A collects all possible is-a relations between such pairs P and N . In the algorithm one such pair is chosen to be added to the ontology. Therefore, there is an individual x and named concepts P and N such that x:P and x:¬ N are statements in A e , and such that P⊑ N was added to the ontology. By lemma 1 A e is then closed which contradicts with our assumption. This shows that all leaf ABoxes are closed and thus A i⊑ B i can be derived from the knowledge base of the ontology extended with {P 1 ⊑ N 1 , . . ., P m⊑ N m }. ♣

Theorem 1 Any element of Rep(M ) repairs the missing is-a relations in M .
Proof. The previous lemma guarantees that adding any element from Rep(A i , B i ) to KB allows us to derive A i⊑ B i . Therefore, adding one element from each The proposed algorithm returns minimal solutions for every missing is-relation. In our setting a solution is minimal if it contains only necessary information for repairing a missing is-a relation.

Definition 2 Let KB be a knowledge base representing ontology O and A⊑ B
a missing is-a relation. A repairing action {C 1⊑ D 1 , . . . , C n⊑ D n } is said to be minimal if it holds that KB ∪{C 1⊑ D 1 , . . . , C n⊑ D n } |= A⊑ B and there is no

Optimization
The basic algorithm may produce many redundant solutions already in step 1. For instance, if the root node in the completion graph contains x:A and x:¬B with A and B named concepts, then A⊑ B appears in every open leaf ABox as a possible way of closing that ABox. To deal with this issue we modify the algorithm such that at each node with an open ABox it generates P os xj and N eg xj . However, P os xj and N eg xj only contain the concepts that are not already in a P os xj and N eg xj related to an ancestor node. For instance, if A ∈ P os x is related to the root node, then A will not appear in any P os x related to another node. For each ABox we then generate a set R A = x { P⊑ N } where P ∈ P os x for the current node or any ancestor node, N ∈ N eg x for the current node or any ancestor node, and at least one of P and N occurs in the current node. This allows us to reduce the redundancy in step 1. An open leaf ABox can now be closed by using an element from R A from the leaf node or from any ancestor node. When generating repairing actions in step 1.5 we then make sure that when an element related to a non-leaf node is chosen, that no additional element from any descendant of that node is selected. For instance, if any element from the root's R A is chosen, then no other elements should be chosen.
As an example, let us reconsider the computation of the repairing actions related to MyPizza⊑ FishyMeatyPizza for the acyclic terminology in Figure 2.
In the optimized version of the algorithm, we compute P xj , N xj and R A for every open ABox (see Figure 15). The root ABox (ABox 1 in Figure 13) has statements of the forms x j :A and x j :¬A and we thus create Pos x = {MyPizza, Pizza}, Neg x = {FishyMeatyPizza}, Pos y = {AnchoviesTopping, AnchoviesT opping, PizzaTopping}, Neg y = ∅, Pos z = {ParmaHamTopping, P armaHamT opping, PizzaTopping}, Neg z = ∅. This leads to R A1 = {MyPizza⊑ FishyMeatyPizza, Pizza⊑ FishyMeatyPizza} for ABox 1. We also know now that any element of the R A1 will close all leaf nodes. For Abox 1.2 the new statements of the form x j :A and x j :¬A (i.e. not occurring in an ancestor) are y:¬FishTopping and z:¬FishTopping. Therefore, we create Pos x = ∅, Neg x = ∅, Pos y = ∅, Neg y = {FishTopping}, Pos z = ∅, Neg z = {FishTopping} for Abox 1.2. R A1.2 for Abox 1.2 contains the new ways to close this ABox (i.e. ways not occurring in ancestor nodes) and contains AnchoviesTopping⊑ FishTopping, PizzaToppinġ ⊑ FishTopping, and ParmaHamTopping⊑ FishTopping. We now know that any of these will close all leaf ABoxes of Abox 1.2. After all R A are computed for all open ABoxes, a leaf node can be closed using an element from its R A or any R A related to an ancestor node. For instance, ABox 1.2.2.2 can be closed using any element from R A1.2.2.2 , R A1.2.2 , R A1.2 and R A1 . When creating repairing actions we then make sure that when an element related to a non-leaf node is chosen, that no additional element from any descendant of that node is selected to close any leaf ABoxes that are descendants of that non-leaf node. For instance, if AnchoviesTopping⊑ FishTopping related to ABox 1.2 is chosen, then no additional element is chosen to close any leaf ABoxes that are descendants of Abox 1.2.

Extension
The algorithm can be extended to generate additional repairing actions for every individual missing is-a relation. In step 1.5 if A⊑ B is used as one of the is-a relations in a repairing action then also S⊑ T where S is a super-concept of A and T is a sub-concept of B could be used. Therefore, the extended algorithm generates two sets of concepts for every is-a relation A⊑ B in a repairing action, Source set containing named super-concepts of A and Target set containing named sub-concepts of B. Further, to not introduce non-validated equivalence relations where in the original ontology there are only is-a relations, we remove the super-concepts of B from Source, and the sub-concepts of A from Target.
Alternative repairing actions for a repairing action {A 1⊑ B 1 , . . ., A n⊑ B n } are then repairing actions . This extension allows the algorithm to produce more informative repairing actions.
Next, we prove the correctness of the proposed extension.

Theorem 3 If a missing is-a relation A⊑ B is repaired by a repairing action
{C 1⊑ D 1 , . . . , C n⊑ D n } then A⊑ B will also be repaired by {S i⊑ T i |∀i : 1..n : Proof. Let KB be the knowledge base of the original ontology. As {C 1⊑ D 1 , . . ., C n⊑ D n } is a repairing action for A⊑ B, we know that KB ∪ {C 1⊑ D 1 , . . ., C n⊑ D n } |= A⊑B.
To prove that A⊑ B is repaired by {S i⊑ T i |∀i : 1..n : we need to show that A⊑ B can be derived from the knowledge base of the extended ontoloy KB ∪ {S i⊑ T i |∀i : 1..n : As S i ∈ Source(C i , D i ), we know that KB |= C i⊑ S i . Further as T i ∈ T arget(C i , D i ), we know that KB |= T i⊑ D i . Therefore, KB ∪ {S i⊑ T i |∀i : 1..n : This shows that KB ∪ {S i⊑ T i |∀i : 1..n : S i ∈ Source(C i , D i ) ∧ T i ∈ T arget(C i , D i )} entails all statements that KB ∪ {C 1⊑ D 1 , . . ., C n⊑ D n } entails and thus also A⊑ B.

Implementation
We have implemented a system that supports the user to repair missing is-a relations. In our system the user loads the ontology and the missing is-a relations from the 'File' menu. The missing is-a relations are then shown in a drop-down list (e.g. MyPizza⊑ FishyMeatyPizza 9 in the second drop-down list in Figure  11). The user then chooses a missing is-a relation to repair. 10 At any time the user can switch between different missing is-a relations. Once a missing is-a relation is chosen for repairing the user generates repairing actions for it by clicking 9 In the system C⊑ D is shown as C → D. 10 As we repair one is-a relation at a time, there may be some redundancy in the solutions. the 'Generate Repairing Actions' button. This covers step 1 in Figure 4 and was implemented in Java using Pellet (version 2.3.0) [31]. The satisfiability checker in Pellet was modified in order to extract full completion graphs. Furthermore, to increase performance and account for higher level of non-determinism, ontologies are first passed through Pellint [22] before running the algorithm. The computed repairing actions are shown in the drop-down list under the button. Each repairing action consists of one or more is-a relations. In Figure 11 the user has chosen to repair MyPizza⊑ FishyMeatyPizza and the system has generated three repairing actions that do not introduce incoherence ({MyPizza⊑ FishyMeatyPizza}, {AnchoviesTopping⊑ FishTopping, ParmaHamTopping⊑ MeatTopping}, and {AnchoviesTopping⊑ MeatTopping, ParmaHamTopping⊑ FishTopping}). To repair this missing is-a relation the user has to succesfully deal with at least one of the repairing actions, i.e. add all is-a relations (or more informative is-a relations from Source and Target) in at least one of the repairing actions to the ontology. In Figure 11 the user has chosen the second repairing action. When repairing actions are added to the ontology, they will make the missing is-a relation derivable. However, it is not guaranteed that all the isa relations in the repairing actions are also valid with respect to the domain. Therefore, a domain expert needs to validate the is-a relations in the repairing actions. When the user clicks the 'Validate is-a Relations in Repairing Action' button, a pop-up window ( Figure 11) appears where the user can mark all the is-a relations that are correct with respect to the domain model. The repairing actions for all missing is-a relations and the ontology are updated according to the results of the validation. If an is-a relation is validated as incorrect according to the domain, all repairing actions that contain this incorrect is-a relation, for this and for all other missing is-a relations, are removed from the lists of the repairing actions. When an is-a relation is validated as correct it is added to the ontology and it is marked as correct in all repairing actions for all missing is-a relations. When all is-a relations in the current repairing action are validated as correct, they are shown in the last drop-down list ( Figure 12). Now the user can repair them one by one.
For each is-a relation within the repairing action the Source and Target sets are generated and displayed on the left and the right hand sides, respectively, within the panel under the drop-down lists ( Figure 12). Both panels have zoom control and can be opened in a separate window. The concepts in the is-a relation under consideration are highlighted in red, existing asserted and inferred is-a relations are shown in grey, not yet repaired missing is-a relations in blue and is-a relations that were previously added for repairing missing is-a relations in black. In order to repair the is-a relation the user has to choose one concept from each of the sets and click the 'Repair' button. In Figure 12 the user has chosen to repair ParmaHamTopping⊑ MeatTopping with ParmaHamToppinġ ⊑ HamTopping. Upon repair the ontology is updated, i.e. the chosen is-a relation (ParmaHamTopping⊑ HamTopping) is added to the ontology. A red label next to the drop-down list shows the status (Repaired or Not Repaired) of the selected is-a relation. When all is-a relations within a repairing action are repaired the missing is-a relation is marked as repaired ('This relation is already repaired' label in Figure 12). The other repairing actions are still available for review by the user. These may give information about other possible missing is-a relations. The user can also revoke repairing actions (through the 'Revoke Repairing Actions' button). If the user revokes the repairing action, the missing is-a relation may become not repaired again and the is-a relations within the repairing action are marked as not repaired. All changes in the ontology are revoked and the user can start repairing this missing is-a relation again in the way just described.
Example run As an example run, consider the ontology in Figure 1 and missing is-a relations MyPizza⊑ FishyMeatyPizza and MyFruttiDiMare⊑ NonVegetar-ianPizza. After loading the ontology and the missing is-a relations, we can choose a missing is-a relation to repair. Assume we choose MyFruttiDiMare⊑ NonVeg-etarianPizza and click the 'Generate Repairing Actions' button. The system will show three repairing actions in the drop-down list: {MyFruttiDiMare⊑ NonVeg-etarianPizza}, {AnchoviesTopping⊑ FishTopping}, and {AnchoviesTopping⊑ MeatTopping}. We can choose to deal with AnchoviesTopping⊑ MeatTopping and validate this to be incorrect with respect to the domain. In this case all repairing actions containing this is-a relation will be removed. We could then choose AnchoviesTopping⊑ FishTopping and validate it to be correct. All is-a relations in this repairing action (i.e. AnchoviesTopping⊑ FishTopping) are validated to be correct and thus we can continue with the repair of AnchoviesTop-ping⊑ FishTopping. In this small example the Source set only contains An-choviesTopping and the Target set only contains FishTopping. Therefore, we click on these concepts and the 'Repair' button. AnchoviesTopping⊑ FishTopping will be marked as repaired and also the missing is-a relation MyFruttiDi-Mare⊑ NonVegetarianPizza will be marked as repaired.
We can then start repairing MyPizza⊑ FishyMeatyPizza. The system would have generated as repairing actions that do not introduce incoherence {MyPizzȧ ⊑ FishyMeatyPizza}, {AnchoviesTopping⊑ FishTopping, ParmaHamToppinġ ⊑ MeatTopping} and {AnchoviesTopping⊑ MeatTopping, ParmaHamToppinġ ⊑ FishTopping}. However, as we earlier already validated AnchoviesTopping⊑ MeatTopping to be incorrect with respect to the domain, the third repairing action has already been removed. When we choose the second repairing action, AnchoviesTopping⊑ FishTopping is already marked as correct (because of earlier validation) and only ParmaHamTopping⊑ MeatTopping needs to be validated. We validate this as correct and then choose to repair it. The Source set in this small example contains ParmaHamTopping and the Target set contains HamTopping and MeatTopping. Although we can add ParmaHamToppinġ ⊑ MeatTopping, it is more informative (and correct with respect to the domain) to add ParmaHamTopping⊑ HamTopping. We therefore choose the latter. All is-a relations in this repairing action are then repaired and thus also MyPizza⊑ FishyMeatyPizza.

Related work
Debugging ontologies Detecting missing is-a relations can be done in a number of ways (see Section 1). There is, however, not much work on the repairing of missing is-a structure. In [20] we addressed this in the setting of taxonomies.
There is more work on the debugging of semantic defects. Most of it aims at identifying and removing logical contradictions from an ontology. Standard reasoners are used to identify the existence of a contradiction, and provide support for resolving and eliminating it [9]. In [29] minimal sets of axioms are identified which need to be removed to render an ontology coherent. In [16,15] strategies are described for repairing unsatisfiable concepts detected by reasoners, explanation of errors, ranking erroneous axioms, and generating repair plans. In [10] the focus is on maintaining the consistency as the ontology evolves through a formalization of the semantics of change for ontologies. In [24] and [13] the setting is extended to repairing ontologies connected by mappings. In this case, semantic defects may be introduced by integrating ontologies. Both works assume that ontologies are more reliable than the mappings and try to remove some of the mappings to restore consistency. The solutions are often based on the computation of minimal unsatisfiability-preserving sets or minimal conflict sets. The work in [28] further characterizes the problem as mapping revision. Using belief revision theory, the authors give an analysis for the logical properties of the revision algorithms. Another approach for debugging mappings is proposed in [32] where the authors focus on the detection of certain kinds of defects and redundancy. The approach in [14] deals with the inconsistencies introduced by the integration of ontologies, and unintended entailments validated by the user.
Work that deals with both modeling and semantic defects includes [5] where the authors propose an approach for detecting modeling and semantic defects within an ontology based on patterns and antipatterns. Some suggestions for repairing are also given. In [19] we provided a method to detect and repair wrong and missing is-a structure in taxonomies connected by mappings.
A different setting is the area of modular ontologies where the ontologies are connected by directional mappings and where knowledge propagation only occurs in one direction. Regarding the detection of semantic defects, within a framework based on distributed description logics, it is possible to restrict the propagation of local inconsistency to the whole set of ontologies (e.g. [30]).
Abductive reasoning in description logics In [8] four different abductive reasoning tasks are defined -(conditionalized) concept abduction, ABox abduction, TBox abduction and knowledge base abduction. Concept abduction deals with finding sub-concepts. Abox abduction deals with retrieving abductively instances of concepts or roles that, when added to the knowledge base, allow the entailment of a desired ABox assertion. Knowledge base abduction includes both ABox and TBox abduction.
Most existing approaches for DL abduction focus on ABox and concept abduction and are mostly based on existing proof techniques such as semantic tableaux and resolution. Since the number of possible solutions is very large, the approaches introduce constraints. The work in [17] proposes a goal-oriented approach where only actions which contribute to the solution are chosen in the proof procedures. The method is both complete and sound for consistent and semantically minimal solutions. Since the set of solutions can contain some inconsistent and non-minimal solutions additional checks are required. A practical approach for ABox abduction, based on abductive logic programming, was proposed in [7]. In order to use existing abductive logic programming systems it is necessary to do a transformation to a plain Datalog program. The solutions are consistent and minimal given a set of abduciles. However, the approach does not guarantee completeness since the translation to a Datalog program is approximate and in some cases a solution would not be found. An approach for conditionalised concept abduction that uses a variation of the semantic tableaux and two labeling functions was proposed in [4]. The two labeling functions T () and F () represent true and false formulas in a tableaux where the solutions are formed from concepts which have at least one constraint in F() of every open branch. This choice is non-deterministic and can be used to select solutions based on some criteria. The algorithm also contains a consistency check which implies that produced solutions are always consistent.
There has not been much work related to TBox abduction, which is the most relevant abduction problem for this paper. The work in [12] proposes an automata-based approach to TBox abduction using abduciles representing axioms that can appear in solutions. It is based on a reduction to the axiom pin-pointing problem which is then solved with automata-based methods. A PTIME algorithm is proposed for the language EL.
All of the presented approaches to description logic abduction work with relatively inexpressive ontologies, such as EL and ALC. However, some recent work [6] describes a type of conditionalised concept abduction called structural abduction which is applicable to SH.

Conclusion
This paper formalized repairing the is-a structure in ALC acyclic terminologies as a generalized TBox abduction problem, provided a solution based on semantic tableaux, and discussed a system.
There are a number of interesting aspects for future work. First, we intend to extend the algorithm to deal with more expressive ontologies. Further, it may be useful to consider also solutions introducing incoherence as they may lead to the detection of other kinds of modeling defects such as wrong is-a relations. In this case we do not assume anymore that the existing structure is correct. As a domain expert may need to deal with many possible solutions, other useful extensions are mechanisms for ranking the generated repairing actions and among those recommending repairing actions, e.g. based on domain knowledge.