The formal de nition 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.
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 di erently, abductive reasoning is generally used to generate hypotheses about the possible or plausible causes of some phenomenon. Typical uses of abduction are in the elds of medical diagnosis, fault diagnosis and criminal investigation.
In formal logic, an abduction problem is normally speci ed 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 in nite number of solutions to an abduction problem. Various criteria have been de ned for this purpose, for example consistency { a solution should not introduce a contradiction 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.
Di erent forms of abduction have been de ned formally in di erent logics.
In their programmatic paper, Elsenbroich et al. [
In this paper, we describe an algorithm for performing a simpli ed 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 [
Section 2 speci es some of the DL terminology used in this paper and gives an overview of the standard tableau algorithm for ALC. Section 3 includes a de nition 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
In this section, we rstly 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 de nitions of the syntax and semantics of ALC in
particular, and for a more detailed speci cation of the tableau algorithm, the
reader is referred to the Description Logic Handbook [
A knowledge base K is consistent if it admits a model. A concept is unsatis able 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 j= . In an abuse of notation, we often write K j= where is a set of assertions and/or axioms. By this we mean that K j= for all 2 .
The tableau algorithm is a decision procedure for the consistency of a knowledge base. It tries to nd (by a depth- rst 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 :C tD(a) and let : ('; a) be the assertion C u: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 [ f ('; a) : ' 2 T and a used in Ag. (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 t D(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 f k; : kg, 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 = f 1; :::; n0 g is saturated, in which case the algorithm terminates.
If the axioms in the knowledge base form a so-called cyclic TBox, in nite
branches can occur, but this can be addressed by a technique called blocking [
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 [
Attempts have been made to de ne 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 [
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 j= 0. (c) Strong semantic minimality : There is no non-equivalent solution 0 such that K [ j= K [ 0.
Note that these notions of minimality are de ned 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 semantically minimal solution is semantically minimal.
Proof. (a) Let E be an equivalence class of semantically minimal solutions, and 2 E. Let 0 be a solution which is a syntactically minimal subset of . Since 0 , j= 0. But since is a semantically minimal solution such that j= 0, 0 must be equivalent to (by de nition 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 de nition of semantic minimality, there is a non-equivalent solution 0 such that j= 0. Therefore K [ j= K [ 0. In other words, is not a strong semantically minimal solution. tu 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 de nition induces a partial ordering on the set of semantically minimal solutions. We say that a solution is closer to strong semantic minimality than a solution 0 if K [ 0 j= K [ and K [ 6j= K [ 0. 4
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 de nition 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 [fA1 v A2g, 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 [ fA1 v A2g j= '.
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 [
Finally, as a post-processing step, the algorithm tests all solutions for consistency, relevance and semantic minimality.
We now give a more formal speci cation 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 j 9R:> D ::= L j 8R:?
L ::= A j :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 quanti ers, we would either lose completeness or be forced to make the algorithm considerably more sophisticated.
Given a knowledge base K and an axiom ' in ALC, do the following: 1. Execute the standard tableau algorithm for testing whether K j= '. Whenever 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 9R:> v L and L v 8R:? to i.
(c) For each assertion R(a; b) in i0, add 9R:> v 8R:? to i. 3. Generate all solutions obtainable by picking an axiom i from each i such that = f 1; :::; m0 g 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 9R:> v L and L v 8R:?. 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 solution entails the observation '. If j= ', discard . (iii) Semantic minimality: Use the standard tableau algorithm to compare pairs of solutions and 0 for entailment. If j= 0, discard .
We now present a few examples that illustrate the solutions that these steps generate: Example 1: Let K = fA1 v A2g 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 fA1 u :A3(c); :A1 t A2(c)g. { 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: fA1(c); :A3(c); :A1(c)g and fA1(c); :A3(c); A2(c)g. { From the set for the open branch, step 2(a) generates the following set of axioms from which solutions will be built: fA1 v A3; A1 v :A2; A2 v A3g.
Steps 2(b) and (c) are not applied since there are no role assertions involved. { Step 3 generates the following solutions: fA1 v A3g; fA1 v :A2g and fA2 v
A3g. { The post-processing step rejects solutions that are not relevant (i.e. that entail the observation), namely fA1 v A3g.
This leaves two solutions, namely fA1 v :A2g and fA2 v A3g. Note that although = fA1 v :A2g makes A1 unsatis able w.r.t. K [ , this does not violate the satis ability requirement for concepts in the observation in Def. 1.} Example 2: Let K = fA1 v 9R:A2g and ' = A1 v 9R:A3. An obvious solution to hK; 'i is A2 v A3. The algorithm determines this as follows: { The algorithm rstly internalises and negates ' and internalises the single axiom in K to form the initial set of assertions fA1 u 8R::A3(c); :A1 t 9R:A2(c)g. { This tableau requires blocking to avoid repeated application of the 9 rule, and occurs when the 9 rule is applied for the second time. { The tableau has two open branches, with the following sets of role and literal assertions, respectively: fA1(c); R(c; d1); A2(d1); :A3(d1); :A1(d1)g and fA1(c); R(c; d1); A2(d1); :A3(d1); R(d1; d2); A2(d2)g. { Step 2(a) generates A2 v A3, A2 v A1 and :A1 v A3, step 2(b) generates 9R:> v :A1 and step 2(c) generates 9R:> v 8R:? to form the rst set of axioms from which solutions will be built. Similarly, the second set is fA2 v A3, 9R:> v :A1, 9R:> v :A2, 9R:> v A3; 9R:> v 8R:?g. { Step 3 generates the following solutions from these sets: fA2 v A3g, fA2 v A1; 9R:> v :A2g, fA2 v A1; 9R:> v A3g, f:A1 v A3; 9R:> v :A2g, f:A1 v A3; 9R:> v A3g, f9R:> v :A1g and f9R:> v 8R:?g.
Note once again that f9R:> v :A1g makes A1 unsatis able w.r.t. K [ . Also, f9R:> v 8R:?g requires role R to be empty. In other words, no individuals may be related by R. This also makes A1 unsatis able 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 nd it. 5
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
We can generalise the TBox abduction problem by allowing more than one axiom in the observation: De nition 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[ j= . Consistency and minimality are de ned as for Def. 1, and relevance is de ned as follows: (ii) Relevance: No axiom of is entailed by .
Note that since a set of axioms fC1 v D1; :::; Cn v Dng 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 = fA1 v A2g and solution to hK; i is fA3 v A1; A4 v A1g. = fA3 v A2; A4 v A2g. An obvious { The negation of and the internalised axiom in K will be used to form the initial assertion set f(A3 u :A2) t (A4 u :A2)(c); :A1 t A2(c)g. { The tableau will have two open branches labelled with fA3(c); :A2(c); :A1(c)g and fA4(c); :A2(c); :A1(c)g respectively. { From these sets, step 2(a) will generate two sets of axioms, namely f:A1 v
A2; A3 v A1; A3 v A2g and f:A1 v A2; A4 v A1; A4 v A2g. { From these sets, step 3 will generate the solutions f:A1 v A2g; fA3 v A1; A4 v A1g; fA3 v A1; A4 v A2g; fA3 v A2; A4 v A1g and fA3 v A2; A4 v A2g. { fA3 v A1; A4 v A2g; fA3 v A2; A4 v A1g and fA3 v A2; A4 v A2g are not relevant because they contain (and therefore entail) axioms in the observation.
This leaves two solutions, namely f:A1 v A2g and fA3 v A1; A4 v A1g. Note that, together with the original knowledge base, the rst solution makes A2 equivalent to >. } 5.2
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 = fA1(a); A1 v A2g and = fA3(a)g. Two obvious solutions to hK; i are fA1 v A3g and fA2 v A3g.
The algorithm will negate and internalise the single axiom in K to form the initial set of assertions f:A3(a); A1(a); :A1 t A2(a)g. The t-rule will be applied, creating one closed branch and one open branch with the labelling f:A3(a); A1(a); A2(a)g. Step 2(a) will generate the set fA1 v A3; A2 v A3; A1 v :A2g, and step 3 will generate solutions comprising one of each of the axioms in this set. The post-processing step will reject the solution fA1 v :A2g as it contradicts the knowledge base. } Example 5: Let K = fR(a; b)g and = fA(a)g. An obvious solution to hK; i is f9R:> v Ag.
The algorithm will negate the observation and start with the set of assertions f:A(a); R(a; b)g. This set is already saturated, so steps 2(b) and (c) will generate the axioms 9R:> v A and 9R:> v 8R:?. Step 3 will therefore generate the solutions f9R:> v Ag and f9R:> v 8R:?g. 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 involve di erent individual names, e.g. fC1(a1); :::; Cn(am)g. DL syntax does not allow us to express the negation of a set of assertions involving di erent individuals 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 assertions f:C1(a1); :::; :Cn(am)g, 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
In this section, we present theoretical results stating the soundness and completeness 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 [ j= ' will close. tu Theorem 2. (Completeness) Algorithm 1 nds all semantically minimal solutions 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 j= '. 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 . tu Remark: Theorem 1 does not state that Alg. 1 only nds 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 [
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 [
Hence, altogether we consume exponential space.
Further, the post-processing phase is reducible to a nite sequence of
standard entailment problems, of ExpTime-complete complexity in ALC or possibly
lower in the restricted language [
There are some obvious optimisations that would improve the e ciency 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 performed, 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
In this paper, we have described how to implement a restricted form of TBox abduction in ALC using a modi ed 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. backjumping 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
This work is based on research supported in part by the National Research Foundation of South Africa (Grant No. 85482).