TBox Abduction in ALC Using a DL Tableau Ken Halland12 , Katarina Britz2 and Szymon Klarman2 1 School of Computing, University of South Africa, Pretoria, South Africa 2 Centre for Artificial Intelligence Research: UKZN and CSIR Meraka Institute, South Africa hallakj@unisa.ac.za, abritz@csir.co.za and sklarman@csir.co.za Abstract. The formal definition of abduction asks what needs to be added to a knowledge base to enable an observation to be entailed. TBox abduction in description logics (DLs) asks what TBox axioms need to be added to a DL knowledge base to allow a TBox axiom to be entailed. We describe a sound and complete algorithm, based on the standard DL tableau, that takes a TBox abduction problem in ALC and generates solutions in a restricted language. We then show how this algorithm can be enhanced to deal with a broader range of problems in ALC. Keywords: Description logics, abduction, tableau algorithms 1 Introduction Abduction can be viewed as a form of non-standard reasoning where explanations are sought for certain observations in the context of some background knowledge. Stated differently, abductive reasoning is generally used to generate hypotheses about the possible or plausible causes of some phenomenon. Typical uses of abduction are in the fields of medical diagnosis, fault diagnosis and criminal investigation. In formal logic, an abduction problem is normally specified in terms of an observation (in the form of one or more statements) which is not entailed by some background knowledge (in the form of a knowledge base), and asks what needs to be added to the background knowledge to entail the observation. The biggest problem is how to narrow down the possibly infinite number of solutions to an abduction problem. Various criteria have been defined for this purpose, for example consistency – a solution should not introduce a contradic- tion with the background knowledge, relevance – a solution should be expressed in terms of the background knowledge, i.e. it should not independently entail the observation, and minimality – a solution should not hypothesize more than necessary. Different forms of abduction have been defined formally in different logics. In their programmatic paper, Elsenbroich et al. [6] define and describe various forms of abduction in description logics (DLs). Among these is TBox abduction, which is useful for repairing missing subsumptions to debug a knowledge base. In this paper, we describe an algorithm for performing a simplified form of TBox abduction, where the knowledge base and observation are in the DL ALC, but the solutions are in a restricted language. The algorithm is sound and complete with respect to the restricted language and a minimality criterion. This extends previous work on ABox abduction [7]. Section 2 specifies some of the DL terminology used in this paper and gives an overview of the standard tableau algorithm for ALC. Section 3 includes a definition of TBox abduction, and Section 4 describes an algorithm based on the standard algorithm to perform TBox abduction in ALC. Section 5 explains how our abduction algorithm can be enhanced to deal with a broader range of abduction problems, and Section 6 provides an analysis of this algorithm in terms of its soundness, completeness and complexity. Finally, Section 7 discusses the prospects for future work. 2 Preliminaries In this section, we firstly highlight some DL terminology relevant to our purposes. We then give a general description of the standard tableau algorithm for DLs and highlight aspects that are important for our current purposes. For details of DLs in general, for the definitions of the syntax and semantics of ALC in particular, and for a more detailed specification of the tableau algorithm, the reader is referred to the Description Logic Handbook [1]. A knowledge base K is consistent if it admits a model. A concept is unsatisfiable w.r.t. a knowledge base K if its interpretation is empty in all models of K. An ABox assertion or TBox axiom α is entailed by a knowledge base K if α is true in all models of K, in which case we write K |= α. In an abuse of notation, we often write K |= Ω where Ω is a set of assertions and/or axioms. By this we mean that K |= α for all α ∈ Ω. The tableau algorithm is a decision procedure for the consistency of a knowledge base. It tries to find (by a depth-first search) a model of the knowledge base by applying so-called expansion rules. The expansion rules only apply to assertions, so before the algorithm starts, the axioms in the knowledge base are converted to concept assertions by a process called internalisation. These assertions are added to the set of assertions on which the algorithm commences its work. The algorithm repeatedly attempts to apply the expansion rules to the assertions in this set until either a clash occurs (i.e. the set contains an assertion and its negation) in which case the algorithm backtracks to a splitting point, or until the set is saturated (i.e. no further expansion rules can be applied) in which case the algorithm terminates and reports that the knowledge base is consistent. A branch that ends in a clash is called a closed branch and a branch that ends in a saturated set is called an open branch. If all branches of the tableau are closed, the algorithm reports that the knowledge base is inconsistent. Stated more formally: Given an axiom ϕ = C v D and an individual name a, let µ(ϕ, a) be the assertion ¬CtD(a) and let ¬µ(ϕ, a) be the assertion Cu¬D(a). Then, given a knowledge base K = hT , Ai, the root node of the search tree is labelled with the set of assertions Ψ0 = A ∪ {µ(ϕ, a) : ϕ ∈ T and a used in A}. (If A is empty and there are thus no individual names, a dummy individual is introduced for the purpose of internalisation.) All assertions in Ψ0 are converted to negation normal form. For each node labelled with Ψi , an expansion rule is chosen that can be applied to one or more assertions in Ψi . If the expansion rule is not a splitting rule, one or two simpler assertions are added to form an expanded set Ψi+1 which is used to label the next node. If the expansion rule is a splitting rule (i.e. the t-rule), the algorithm forms two branches, removing the assertion to which the rule was applied (e.g. C tD(a)) and adding its component parts (C(a) or D(a)) to form the sets Ψi+1 and Ψj+1 that label the nodes on each branch. One of the branches is chosen (say the one labelled with Ψi+1 ) and the process is repeated until either the current labelling set contains a clash, i.e. Ψj ⊇ {ψk , ¬ψk }, in which case the algorithm backtracks to node labelled with Ψj+1 , or until no application of an expansion rule would expand the set, i.e. Ψj = {ψ1 , ..., ψn0 } is saturated, in which case the algorithm terminates. If the axioms in the knowledge base form a so-called cyclic TBox, infinite branches can occur, but this can be addressed by a technique called blocking [1]. The algorithm also terminates when a branch is blocked, because the infinite branch represents an infinite model of K and is considered an open branch. The standard algorithm described above performs consistency checking of a knowledge base. It can easily be adapted to perform the related reasoning task of subsumption testing [1], i.e. deciding whether an axiom ϕ is entailed by a knowledge base K, as follows: The assertion ¬µ(ϕ, c) (where c is an individual name that does not appear in K) is added to K and the algorithm described above is executed. If the algorithm reports that K ∪ {¬µ(ϕ, c)} is consistent, we conclude that K 6|= ϕ (and vice versa). 3 TBox Abduction Attempts have been made to define abduction and implement reasoners that can make abductive inferences in many logics, including description logics [4, 5, 7–9]. TBox abduction (as opposed to general or so-called knowledge base abduction) asks what TBox axioms need to be added to a DL knowledge base to allow an observation (also in the form of a TBox axiom) to be inferred [6]: Definition 1. Let L and L0 be DLs, K a knowledge base in L and ϕ = C v D a TBox axiom in L such that C and D are satisfiable concepts w.r.t. K, K does not entail ϕ and K ∪ {ϕ} is consistent. The pair hK, ϕi is called a TBox abduction problem. A set of TBox axioms Θ in L0 is called an abductive solution for hK, ϕi if K ∪ Θ |= ϕ. In general there are many solutions to any TBox abduction problem. We narrow down the solutions in three ways: (i) Consistency: K ∪ Θ is consistent. (ii) Relevance: ϕ is not entailed by Θ. (iii) Minimality: We distinguish three types: (a) Syntactic minimality: No proper subset of Θ is a solution. (b) Semantic minimality: There is no non-equivalent solution Θ0 such that Θ |= Θ0 . (c) Strong semantic minimality: There is no non-equivalent solution Θ0 such that K ∪ Θ |= K ∪ Θ0 . Note that these notions of minimality are defined for the target language L0 . The following proposition states some relationships between the three types of minimality: Proposition 1. (a) Every equivalence class of semantically minimal solutions has at least one syntactically minimal representative. (b) Every strongly seman- tically minimal solution is semantically minimal. Proof. (a) Let E be an equivalence class of semantically minimal solutions, and Θ ∈ E. Let Θ0 be a solution which is a syntactically minimal subset of Θ. Since Θ0 ⊆ Θ, Θ |= Θ0 . But since Θ is a semantically minimal solution such that Θ |= Θ0 , Θ0 must be equivalent to Θ (by definition of semantic minimality) and therefore an element of E. So E contains a syntactically minimal solution. (b) Say Θ is a solution to an abduction problem, but is not semantically minimal. Then, by definition of semantic minimality, there is a non-equivalent solution Θ0 such that Θ |= Θ0 . Therefore K ∪ Θ |= K ∪ Θ0 . In other words, Θ is not a strong semantically minimal solution. t u Of the three types of minimality, semantic minimality is particularly useful for implementing the notion of not hypothesizing more than is necessary to entail an observation. This is built into the algorithm which we describe below, and provides the criterion for its completeness. Syntactic minimality is useful for discarding solutions that contain redundant axioms, and is also built into the algorithm. Strong semantic minimality is more useful for ranking solutions, since the definition induces a partial ordering on the set of semantically minimal so- lutions. We say that a solution Θ is closer to strong semantic minimality than a solution Θ0 if K ∪ Θ0 |= K ∪ Θ and K ∪ Θ 6|= K ∪ Θ0 . 4 Algorithm for TBox Abduction The basic idea is to use the standard tableau algorithm described in Sect. 2 to test whether an observation (in the form of an axiom) is entailed by a knowledge base. If the observation is not entailed (it should not be, by the definition of a TBox abduction problem), at least one branch of the tableau will not close. Any set of axioms that would close all such open branches (if added to the original knowledge base plus the negated observation), would form an abductive solution. This can be illustrated by the following simple example: Say we test whether an observation ϕ is entailed by a knowledge base K, and it is not entailed due to a single open branch containing the assertions A1 (a) and ¬A2 (a). Then, if we were to start the algorithm again to test whether ϕ is entailed by K∪{A1 v A2 }, this branch would be closed, since A1 v A2 would be internalised as ¬A1 tA2 (a), which would create a branch with a clash A1 (a) and ¬A1 (a) and a branch with a clash ¬A2 (a) and A2 (a). A1 v A2 is therefore an abductive solution for hK, ϕi since K ∪ {A1 v A2 } |= ϕ. In the following discussion, we use the term literal to denote an atomic concept or its negation. The symbol L represents an arbitrary literal, and L it’s complement. In other words, L is ¬A if L = A, and A if L = ¬A. Our algorithm for TBox abduction works as follows: Firstly, it tests whether the observation is entailed by the knowledge base using the algorithm described in Sect. 2, but does not stop when an open branch is attained. It stores the current set of role and literal assertions, backtracks to the last splitting point and continues the search for the next open branch. Secondly, for each such set, it generates a set of axioms that (if added to the original knowledge base) would close the branch. Thirdly, using Reiter’s minimal hitting set algorithm [10], it generates solutions from the axiom sets. (A solution contains one axiom to close each open branch.) Finally, as a post-processing step, the algorithm tests all solutions for con- sistency, relevance and semantic minimality. We now give a more formal specification of the algorithm. The algorithm only produces solutions in a restricted language which we call Lmin . This language only allows atomic negation and limited existential and universal restriction (and no conjunctions or disjunctions). Furthermore, axioms of Lmin may only be of the form C v D where C and D are concept descriptions of the following forms: C ::= L | ∃R.> D ::= L | ∀R.⊥ L ::= A | ¬A The expressiveness of this target language is fairly modest since our goal was to provide a complete algorithm based on a standard DL tableau to generate all semantically minimal solutions. For example, if we were to allow concepts within the scope of quantifiers, we would either lose completeness or be forced to make the algorithm considerably more sophisticated. Algorithm 1. (Restricted TBox Abduction) Given a knowledge base K and an axiom ϕ in ALC, do the following: 1. Execute the standard tableau algorithm for testing whether K |= ϕ. When- ever an open branch is attained (labelled by the set Ψi ), store the set Ψi0 consisting of the role and literal assertions from Ψi . Continue until the entire search tree has been traversed. 2. For each Ψi0 , generate a set of axioms Γi from which solutions will be built: (a) For each pair of concept assertions L1 (a) and L2 (a) in Ψi0 , add L1 v L2 to Γi . (b) For each combination of assertions R(a, b) and L(a) in Ψi0 , add ∃R.> v L and L v ∀R.⊥ to Γi . (c) For each assertion R(a, b) in Ψi0 , add ∃R.> v ∀R.⊥ to Γi . 3. Generate all solutions Θ obtainable by picking an axiom γi from each Γi such that Θ = {γ1 , ..., γm0 } is syntactically minimal, i.e. there is no proper subset of Θ that would also contain a representative of each Γi . C Note that step 2(a) generates axioms of the form L v L, and steps 2(a) and (b) generate equivalent (contrapositive) pairs of axioms of the form L1 v L2 and L2 v L1 , and ∃R.> v L and L v ∀R.⊥. All the examples given below ignore axioms of the form L v L and one of each pair of the abovementioned equivalent assertions for the sake of simplicity. This is also discussed in Section 6 as an optimisation step. For the post-processing step, the following is done: (i) Consistency: Use the standard tableau algorithm to test each solution Θ for consistency with K. If K ∪ Θ is inconsistent, discard Θ. (ii) Relevance: Use the standard tableau algorithm to test whether each solu- tion Θ entails the observation ϕ. If Θ |= ϕ, discard Θ. (iii) Semantic minimality: Use the standard tableau algorithm to compare pairs of solutions Θ and Θ0 for entailment. If Θ |= Θ0 , discard Θ. We now present a few examples that illustrate the solutions that these steps generate: Example 1: Let K = {A1 v A2 } and ϕ = A1 v A3 . An obvious solution to hK, ϕi is A2 v A3 . The algorithm determines this as follows: – ϕ is internalised and negated as the assertion A1 u ¬A3 (c). The single axiom in K is internalised and applied to c to form the assertion ¬A1 t A2 (c). The initial set of assertions is therefore {A1 u ¬A3 (c), ¬A1 t A2 (c)}. – The expansion rules of the tableau algorithm are applied and we end up with one closed and one open branch with the corresponding sets of literal assertions: {A1 (c), ¬A3 (c), ¬A1 (c)} and {A1 (c), ¬A3 (c), A2 (c)}. – From the set for the open branch, step 2(a) generates the following set of axioms from which solutions will be built: {A1 v A3 , A1 v ¬A2 , A2 v A3 }. Steps 2(b) and (c) are not applied since there are no role assertions involved. – Step 3 generates the following solutions: {A1 v A3 }, {A1 v ¬A2 } and {A2 v A3 }. – The post-processing step rejects solutions that are not relevant (i.e. that entail the observation), namely {A1 v A3 }. This leaves two solutions, namely {A1 v ¬A2 } and {A2 v A3 }. Note that although Θ = {A1 v ¬A2 } makes A1 unsatisfiable w.r.t. K ∪ Θ, this does not violate the satisfiability requirement for concepts in the observation in Def. 1.♦ Example 2: Let K = {A1 v ∃R.A2 } and ϕ = A1 v ∃R.A3 . An obvious solution to hK, ϕi is A2 v A3 . The algorithm determines this as follows: – The algorithm firstly internalises and negates ϕ and internalises the single axiom in K to form the initial set of assertions {A1 u ∀R.¬A3 (c), ¬A1 t ∃R.A2 (c)}. – This tableau requires blocking to avoid repeated application of the ∃−rule, and occurs when the ∃−rule is applied for the second time. – The tableau has two open branches, with the following sets of role and lit- eral assertions, respectively: {A1 (c), R(c, d1 ), A2 (d1 ), ¬A3 (d1 ), ¬A1 (d1 )} and {A1 (c), R(c, d1 ), A2 (d1 ), ¬A3 (d1 ), R(d1 , d2 ), A2 (d2 )}. – Step 2(a) generates A2 v A3 , A2 v A1 and ¬A1 v A3 , step 2(b) generates ∃R.> v ¬A1 and step 2(c) generates ∃R.> v ∀R.⊥ to form the first set of axioms from which solutions will be built. Similarly, the second set is {A2 v A3 , ∃R.> v ¬A1 , ∃R.> v ¬A2 , ∃R.> v A3 , ∃R.> v ∀R.⊥}. – Step 3 generates the following solutions from these sets: {A2 v A3 }, {A2 v A1 , ∃R.> v ¬A2 }, {A2 v A1 , ∃R.> v A3 }, {¬A1 v A3 , ∃R.> v ¬A2 }, {¬A1 v A3 , ∃R.> v A3 }, {∃R.> v ¬A1 } and {∃R.> v ∀R.⊥}. Note once again that {∃R.> v ¬A1 } makes A1 unsatisfiable w.r.t. K ∪ Θ. Also, {∃R.> v ∀R.⊥} requires role R to be empty. In other words, no individuals may be related by R. This also makes A1 unsatisfiable w.r.t. K ∪ Θ. ♦ Of course, some abductive problems only have solutions that are not consistent or not relevant. An empty knowledge base, for example, cannot have any relevant solutions to any abductive problem. However, as we show in Th. 2, if a problem in ALC has a solution in Lmin , Alg. 1 will find it. 5 Enhancements to the Algorithm As it turns out, Alg. 1 can be used to deal with a broader class of abductive problems than those permitted by Def. 1. Firstly, we can allow multiple TBox axioms in the observation. Secondly, we can enhance the algorithm to deal with concept assertions in the observation. 5.1 Observations Involving Multiple Axioms We can generalise the TBox abduction problem by allowing more than one axiom in the observation: Definition 2. Let L and L0 be DLs, K a knowledge base in L and Φ a set of TBox axioms in L such that no axiom of Φ is entailed by K and K ∪ Φ is consistent. The pair hK, Φi is called a generalised TBox abduction problem. A set of TBox axioms Θ in L0 is called an abductive solution for hK, Φi if K∪Θ |= Φ. Consistency and minimality are defined as for Def. 1, and relevance is defined as follows: (ii) Relevance: No axiom of Φ is entailed by Θ. Note that since a set of axioms {C1 v D1 , ..., Cn v Dn } represents their implicit conjunction, the negation of such a set is equivalent to the assertion (C1 u¬D1 )t ... t (Cn u ¬Dn )(c) for some individual name c not appearing in the knowledge base. Example 3: Let K = {A1 v A2 } and Φ = {A3 v A2 , A4 v A2 }. An obvious solution to hK, Φi is {A3 v A1 , A4 v A1 }. – The negation of Φ and the internalised axiom in K will be used to form the initial assertion set {(A3 u ¬A2 ) t (A4 u ¬A2 )(c), ¬A1 t A2 (c)}. – The tableau will have two open branches labelled with {A3 (c), ¬A2 (c), ¬A1 (c)} and {A4 (c), ¬A2 (c), ¬A1 (c)} respectively. – From these sets, step 2(a) will generate two sets of axioms, namely {¬A1 v A2 , A3 v A1 , A3 v A2 } and {¬A1 v A2 , A4 v A1 , A4 v A2 }. – From these sets, step 3 will generate the solutions {¬A1 v A2 }, {A3 v A1 , A4 v A1 }, {A3 v A1 , A4 v A2 }, {A3 v A2 , A4 v A1 } and {A3 v A2 , A4 v A2 }. – {A3 v A1 , A4 v A2 }, {A3 v A2 , A4 v A1 } and {A3 v A2 , A4 v A2 } are not relevant because they contain (and therefore entail) axioms in the observation. This leaves two solutions, namely {¬A1 v A2 } and {A3 v A1 , A4 v A1 }. Note that, together with the original knowledge base, the first solution makes A2 equivalent to >. ♦ 5.2 Observations Involving Concept Assertions We can generalise Def. 2 further so that the observation can also contain concept assertions. This is illustrated in the following examples: Example 4: Let K = {A1 (a), A1 v A2 } and Φ = {A3 (a)}. Two obvious solu- tions to hK, Φi are {A1 v A3 } and {A2 v A3 }. The algorithm will negate Φ and internalise the single axiom in K to form the initial set of assertions {¬A3 (a), A1 (a), ¬A1 t A2 (a)}. The t-rule will be applied, creating one closed branch and one open branch with the labelling {¬A3 (a), A1 (a), A2 (a)}. Step 2(a) will generate the set {A1 v A3 , A2 v A3 , A1 v ¬A2 }, and step 3 will generate solutions comprising one of each of the axioms in this set. The post-processing step will reject the solution {A1 v ¬A2 } as it contradicts the knowledge base. ♦ Example 5: Let K = {R(a, b)} and Φ = {A(a)}. An obvious solution to hK, Φi is {∃R.> v A}. The algorithm will negate the observation and start with the set of assertions {¬A(a), R(a, b)}. This set is already saturated, so steps 2(b) and (c) will generate the axioms ∃R.> v A and ∃R.> v ∀R.⊥. Step 3 will therefore generate the solutions {∃R.> v A} and {∃R.> v ∀R.⊥}. The latter solution will be rejected because it contradicts the knowledge base, leaving the former which is the one we expected. ♦ Now suppose the observation Φ consists of a set of concept assertions that in- volve different individual names, e.g. {C1 (a1 ), ..., Cn (am )}. DL syntax does not allow us to express the negation of a set of assertions involving different indi- viduals as a single assertion. We could start a separate tableau for each negated assertion and collect the axioms needed to close all open branches of all trees. Alternatively, we could store such a negated set as a special set of negated as- sertions {¬C1 (a1 ), ..., ¬Cn (am )}, where there are implicit disjunctions between the assertions. When the algorithm reaches a point where no other expansion rules can be applied, it picks one (negated assertion) and creates a branch with it. When the algorithm backtracks to this point, the next one is chosen. This works just like an application of the t-rule. 6 Analysis In this section, we present theoretical results stating the soundness and com- pleteness of Alg. 1, analyse its complexity and discuss various optimisations. Theorem 1. (Soundness) All solutions generated by Algorithm 1 are TBox abduction solutions. Proof sketch: By the way solutions are constructed by steps 2(a), (b) and (c) of Alg. 1, we show that any such solution Θ for an abduction problem hK, ϕi will close all the open branches of the tableau. In other words, the tableau for testing K ∪ Θ |= ϕ will close. t u Theorem 2. (Completeness) Algorithm 1 finds all semantically minimal so- lutions in Lmin to a TBox abduction problem in ALC up to logical equivalence. Proof sketch: For any semantically minimal solution Θ to an abduction problem hK, ϕi, we pick a minimal subset of Θ needed to close each open branch of the tableau for testing K |= ϕ. By means of a lemma, we prove that each such set is equivalent to a singleton set. We then show that the algorithm will generate a solution equivalent to the union of these sets, which is also equivalent to Θ. t u Remark: Theorem 1 does not state that Alg. 1 only finds semantically minimal solutions. In fact, it generates some non-semantically minimal solutions, which explains the need for the post-processing step to discard them. The complexity of the standard tableau algorithm for consistency checking with general TBoxes in ALC is NExpTime [3]. But this is because the algorithm only needs to find one open branch by making a series of non-deterministic choices at the splitting points, and the length of each branch is in O(2n ) in the worst case (where n is the size of the input). Algorithm 1, however, generates all open n branches, and this takes double exponential time in the worst case, i.e. O(22 ) different branches. This does not even take into account the time needed to work out the axioms used to build solutions. Nevertheless, we are able to tighten the upper bound to ExpSpace, known to be subsumed by 2ExpTime, by augmenting the algorithm. First, we note that the size of the vocabulary used in the input is not larger than n. The solution language Lmin permits at most polynomially many axioms in n over this vocabulary. Then we can do the following: – Whenever a new open branch is attained, we can generate and store all the axioms in Lmin that can close it rather than the set of role and literal assertions. Then we can dump the branch. – Since there are at most O(2n ) sets of axioms that can be generated from a polynomially sized set, we only need exponential space to store them. – Although in general Reiter’s minimal hitting set algorithm requires space exponential in the number of sets [11], once again, the restricted language limits the number of solutions to at most O(2n ) (the power set of the set of all axioms). Hence, altogether we consume exponential space. Further, the post-processing phase is reducible to a finite sequence of stan- dard entailment problems, of ExpTime-complete complexity in ALC or possibly lower in the restricted language [1]. There are some obvious optimisations that would improve the efficiency of our algorithm. Firstly, one could store only the sets of axioms for each open branch rather than the sets of role and literal assertions (as stated above). Secondly, one could discard equivalent, irrelevant and inconsistent axioms as they are generated (in steps 2(a) and (b)). This would save them from being processed by step 3. Finally, a distributed version of Reiter’s hitting set algorithm could be per- formed, where candidate solutions are built as the sets of axioms are populated. This could involve elimination of duplicate axioms, and whole sets of axioms that are supersets of others. 7 Conclusion and Future Work In this paper, we have described how to implement a restricted form of TBox abduction in ALC using a modified DL tableau. It would be possible to generalise the algorithm to produce solutions in a less restricted language, but not one that could generate all possible solutions in ALC. Future work could look at getting the algorithm to generate more solutions that are also meaningful. Our algorithm does not implement many of the optimisations (e.g. back- jumping and caching) common in DL tableau algorithms. Incorporating these, as well as the optimisations mentioned at the end of Sect. 6, would improve it. This work also promises to be transferable to other more expressive DLs. 8 Acknowledgements This work is based on research supported in part by the National Research Foundation of South Africa (Grant No. 85482). References 1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook, Cambridge University Press (2003) 2. Baader, F., Horrocks, I., Sattler, U.: Chapter 3: Description Logics. In: van Harme- len, F., Lifschitz, V., Porter, B., editors: Handbook of Knowledge Representation, Elsevier (2007) 3. Baader, F., Sattler, U.: Overview of Tableau Algorithms for Description Logics, in Studia Logica, vol 69 (2000) 4. Di Noia, T., Di Sciascio, E., Donini, F.M.: Computing information minimal match explanations for logic-based matchmaking, in Proc. of the 2009 IEEE/WIC/ACM International Joint Conference on Web Intelligence and Intelligent Agent Technol- ogy, vol 02, IEEE Computer Society (2009) 5. Du, J. Qi, G., Shen, Y-D., Pan, J.Z.: Towards practical ABox abduction in large OWL DL ontologies, in Proc. of the 25th AAAI Conference (2011) 6. Elsenbroich, C., Kutz, O., Sattler, U.: A case for abductive reasoning over ontolo- gies, in Proc. of the OWLED’06 Workshop, vol 216 (2006) 7. Halland, K., Britz, K.: ABox abduction in ALC using a DL tableau, in Proc. of SAICSIT 2012, (2012) 8. Klarman, S., Endriss, U., Schlobach, S.: ABox abduction in the description logic ALC, Journal of Automated Reasoning, vol 46:1 (2011) 9. Lambrix, P., Wei-Kleiner, F., Dragisic, Z. Ivanova, V.: Repairing missing is-a struc- ture in ontologies is an abductive reasoning problem, in Proc. of WoDOOM13, (2013) 10. Reiter, R.: A theory of diagnosis from first principles, Artificial Intelligence, vol 32 (1987) 11. Wotawa, F.: A variant of Reiter’s hitting-set algorithm, Information Processing Letters, vol 79 (2001)