The formal de nition of abduction asks what needs to be added to a knowledge base to enable an observation to be entailed by the knowledge base. An observation which is not entailed by the knowledge base will result in open branches in a complete semantic tableau for the entailment. The statements required to close these branches therefore represent a solution to the abductive problem. In this paper we describe how this idea can be implemented for ABox abduction in the description logic ALC. We analyse the limitations of our algorithm and propose re nements to improve the quality of results.
Abduction is a form of non-standard reasoning where explanations are generated for certain observations in the context of some background knowledge. This is as opposed to deduction { the standard form of reasoning where the logical consequences of some knowledge are determined.
A typical use of abduction is in the process of medical diagnosis. Say a patient displays some symptoms. A doctor uses abductive reasoning to generate hypotheses about the possible ailment(s) causing the symptoms. These hypotheses can then be tested by collecting corroborating evidence so that deduction can be used to make a correct diagnosis.
Abductive reasoning is non-monotonic in that the solutions derived from some background knowledge and an observation may no longer hold if we add new statements to the background knowledge.
Di erent forms of abduction have been formally de ned in di erent logics. In
their programmatic paper, Elsenbroich et al [
In particular, Klarman et al [
Syntax: The reader is referred to the Description Logic Handbook [
A knowledge base is a set of statements partitioned into an ABox and a TBox. ABox assertions are statements of the form C(I) and R(I; J ) (called concept assertions and role assertions, respectively), and TBox axioms are statements of the form C v D (sometimes called general concept inclusions, or GCIs).3 The following serves as a running example. Admittedly it is not very good knowledge representation, but we have chosen the given formulation for the sake of illustration.
Example 1: The following knowledge base is intended to express the ideas that In uenza A is a form of in uenza, Malaria vivax is a form of malaria (caused 3 In this and the following speci cations, C and D represent arbitrary concept descriptions, R represents an arbitrary role name, and I and J represent arbitrary individual names. by Plasmodium vivax ), and someone infected with in uenza or malaria will be feverish:
In uenza(FLU A)
Malaria(MAL V)
9infectedWith:In uenza t 9infectedWith:Malaria v Feverish
Semantics: Once again, the reader is referred to the DL Handbook [
An interpretation I is a model of a knowledge base K if all the statements of K are true in I. A concept description C is satis able with respect to a knowledge base K if there is some model of K such that the interpretation of C is not empty. A statement 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 statements. By this we mean that K j= for all 2 . A knowledge base K is consistent if it admits a model. 3
An abduction problem is normally de ned in terms of an observation (in the form of one or more statements) which is not entailed by a theory (i.e. a set of statements), and asks what needs to be added to the theory to entail the observation.
Example 2: Using the knowledge base given in Example 1, say we observe that John is feverish. An abduction problem would be to ask what should be added to the knowledge base to allow us to infer Feverish(JOHN).
We expect abduction to allow us to hypothesize that John is infected with in uenza or he is infected with malaria, i.e. 9infectedWith:In uenza(JOHN) or 9infectedWith:Malaria(JOHN). In fact, more speci c hypotheses would be that he is infected with In uenza A, i.e. infectedWith(JOHN; FLU A), or that he is infected with Malaria vivax, i.e. infectedWith(JOHN; MAL V). The reader might like to check that adding any of these assertions to the knowledge base will allow us to infer Feverish(JOHN).
One problem with a formal de nition of abduction 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. Like other authors [
This is an abductive solution, since if both these statements were added to the knowledge base, it would allow us to infer Feverish(JOHN). However, it would also allow us to make this inference independently of the knowledge base and is therefore not a relevant solution. (Incidentally, the observation itself, in this case fFeverish(JOHN)g, is also always a non-relevant solution, since adding it to the knowledge base would allow the observation to be trivially inferred.) iii. f9infectedWith:In uenza(JOHN); 9infectedWith:Malaria(JOHN)g.
Although this is a valid solution, it is not minimal because it hypothesizes too much, namely that John is infected with both in uenza and malaria. 3.1
ABox Abduction in ALC
As stated in the introduction, attempts have been made to de ne abduction
and implement reasoners that can make abductive inferences in many logics,
including description logics. ABox abduction (as opposed to general or so-called
knowledge base abduction [
The astute reader will note that apart from not being relevant, Example 3 ii is also not an ABox abduction solution, since it contains a TBox axiom. De nition 1. Given a knowledge base K and a set of ABox assertions (both in ALC) such that K does not entail and K [ is consistent, then a set of ABox assertions is an abductive solution for (K; ) if K [ j= .
K [ i. Consistency : K [ is consistent. ii. Relevance: is not entailed by . iii. Minimality : We distinguish two kinds of minimality: (a) Syntactic: No proper subset of is a solution. (b) Semantic: There is no non-equivalent solution 0. 0 such that K [ j= Note that our de nition of semantic minimality induces a partial ordering on the set of solutions, and that there can be a number of semantically minimal (nonequivalent) solutions to a particular abductive problem. We say that a solution is closer to semantic minimality than a solution 0 if K [ 0 j= K [ and K [ 6j= K [ 0.
The Semantic Tableau Algorithm for ALC
For a more detailed description of the semantic tableau algorithm for ALC,
the reader is referred to the Handbook of Knowledge Representation [
The standard semantic tableau algorithm for description logics (and for ALC in particular) tries to nd (i.e. construct) a model of the knowledge base by applying so-called expansion rules to its statements.
The expansion rules only apply to ABox assertions, so before the algorithm can commence, the TBox axioms in the knowledge base must be converted to concept assertions by a process called internalisation.
In ALC, it is possible to specify a knowledge base that has in nite models (by means of a so-called cyclic TBox). This issue is dealt with by a technique called blocking, which essentially detects when more than one individual has the same labelling in the current model.
If the algorithm detects a contradiction (or clash), i.e. the current set of assertions contains a concept assertion and its negation, it backtracks and tries another branch of its search. If it gets to a point where the current set of assertions are saturated, i.e. no more expansion rules can be applied and there is no contradiction, then a model has been found, the algorithm terminates and reports that the original knowledge base is consistent.
The algorithm described above performs consistency checking of a knowledge base. It can easily be adapted to perform the related reasoning task of instance checking, i.e. deciding whether a concept assertion is entailed by a knowledge base, as follows: The negation of the concept assertion being tested is added to the knowledge base and the algorithm described above is executed. If the resulting knowledge base is consistent, we conclude that the assertion is not entailed by the knowledge base (and vice versa). 5
For the purpose of ABox abduction, we perform instance checking of an
observation by means of a so-called extended (or complete) semantic tableau, i.e. a
tableau that doesn't terminate when the rst open branch is attained. Every
time an open branch is attained, the current set of assertions (representing a
model of the original set of assertions) is stored, the algorithm backtracks and
continues its search. Reiter's minimal hitting set algorithm [
Although extendedST implements blocking, this is not used in any way for
the generation of solutions. The argument is as follows: Since ALC has the nite
model property [
Reiter's minimal hitting set algorithm (in general) is NP-complete [
Finally, the algorithm invokes the functions consistentST and relevantST twice for each candidate solution. Although the space required for relevantST is only polynomial (because it does not deal with the TBox), consistentST is in ExpTime in the worst case because it must deal with the TBox. Since the number of hitting sets is polynomial in the size of the initial assertion set, the total space requirement for this process is in ExpTime.
The entire algorithm is therefore in ExpTime. 5.2
Taking De nition 1 as the standard for ABox abduction in ALC, Algorithm 1 is sound but not complete.
It is sound because all solutions that it generates are proper abduction solutions according to the de nition. Consider the following argument: Each solution is a set comprised of the complements of assertions in the open branches of the extended semantic tableau, such that each open branch has a representative in the solution. So if the assertions of such a solution were to be added to the knowledge base (and the satis ability test were to be performed again), all branches would close, indicating that the observation is now entailed by the knowledge base. This is precisely the de nition of an abduction solution.
It is not complete due to the problems detailed in Section 6. One should not be surprised at this because abductive inference is notoriously incomplete due to the often in nite number of solutions to an abduction problem. Narrowing down the spectrum of solutions by means of criteria such as consistency, relevance and minimality only partially addresses this issue. Many solutions within these criteria are di cult to obtain, particularly by means of the techniques described here. In Section 6 we propose workarounds to make the algorithm more complete.
The algorithm described in Section 5 is \nave" in that it doesn't deal with all observations and it doesn't generate all possible solutions allowed by our de nition. In particular, the algorithm has the following weaknesses:
6.1
Contrary to De nition 1, our algorithm does not allow more than one concept assertion in the observation. This is because an observation consisting of multiple assertions is really a conjunction of assertions, and the rst step of the algorithm is to add the negation of the observation, which is in e ect a disjunction of the negations of its individual assertions. We cannot express such a disjunction of assertions in DL syntax when the assertions involve di erent individuals. (This is not a problem for multiple concept assertions about the same individual, e.g. C(I) and D(I) can be negated as :C t :D(I).)
Furthermore, the observation may not contain any role assertions, because ALC syntax doesn't allow negated role assertions. So we cannot deal with observations such as hasSymptom(JOHN; INTERMITTENT FEVER). (It is true that in many cases this situation could be handled by alternative modelling, e.g. 9hasSymptom:IntermittentFever(JOHN), but there might be situations where this is not practical or desirable.)
Neither of these situations are a problem for Klarman et al [
Proposed Workaround: A brute-force method of dealing with multiple assertions in the observation would be to execute the algorithm once for each such assertion, harvest all the models from all open branches of all executions, and then process them as normal. This, however, would involve a lot of duplication (processing the rest of the assertions repeatedly). One way to avoid such duplication would be to keep the complemented assertions of the observation in a separate list from the other assertions. (The set of complemented assertions would represent a disjunction of assertions, whereas the other set would represent a conjunction of assertions { as normal.) Then when no other expansion rules can be applied to the normal set, the algorithm can branch for one of the complemented assertions.
The negation of a role assertion R(I; J ) can be accounted for by two
assertions: 8R:A(I) and :A(J ), where A is a dummy concept name not occurring in
the knowledge base. Adding these two assertions to the initial set of assertions
will have the same e ect as adding the negation of the role assertion. Assertions
involving such dummy concept names will need to be ignored for the purposes
of determining abductive solutions.
Our algorithm su ers from the same problem as Klarman's [
Proposed Workaround: One reason for this problem is that our algorithm only considers unexpanded concept assertions for forming solutions. Allowing expandable concept assertions to be selected for solutions would allow some disjunctions, but not all. For example, say we replaced the axiom of Example 1 with the two axioms 9infectedWith:In uenza v Feverish and 9infectedWith:Malaria v Feverish. In this case, the solution with the disjunction above would be a valid solution, but would not be generated.
One could construct some such solutions from their constituent parts, e.g. C t D(I) could be constructed from C(I) and D(I), but more complex solutions involving disjunctions inside quanti ers would be more di cult, e.g. 9R:(C t D)(I) will not be generated when 9R:C(I) and 9R:D(I) are.
Klarman et al [
A more serious weakness is that the algorithm will never generate solutions involving role assertions. So the more speci c solutions mentioned in Example 2, namely infectedWith(JOHN; FLU A) and infectedWith(JOHN; MAL V), are unattainable with our algorithm.
Stated more generically: Consider a knowledge base containing the ABox assertion 8R:A(I), and say we want an abductive explanation of the observation A(J ). An obvious solution is R(I; J ). But our abductive solutions are always the complements of assertions needed to close the open branches of a semantic tableau. Since the tableau algorithm does not infer negated role assertions, this solution will not be generated.
Proposed Workaround: One way would be to add the assertion R(I; J ) to
a solution whenever the \pattern" f8R:A(I); :A(J )g occurs in a open terminal
branch. However, although this will enable some role assertions to be included
in solutions, it will not generate all: Adding the role assertion R(I; J ) to a
knowledge base will cause an open branch containing f8R:C(I); :D(J )g, where
C is disjoint from D, to close, so it should form part of an abductive solution
whenever this pattern occurs. Such a pattern could be di cult to recognise, and
the easiest way to deal with this would probably be to allow nominals in the
language, since a negated role assertion :R(I; J ) can then be expressed as a
concept assertion, namely 8R::fJ g(I) [
Using the observation of Example 2, the algorithm now generates the solutions 9infectedWith:In uenza(JOHN) and 9bloodTestIndicates:Plasmodium(JOHN). One of the solutions we got previously, namely 9infectedWith:Malaria(JOHN) has gone! In fact, a solution that is closer to semantic minimality has been lost. Proposed Workaround: Many such solutions that are closer to semantic minimality can be obtained by allowing expanded concept assertions as part of solutions (including the above example). However, this will not solve all problems: Consider the knowledge base consisting of TBox = fA1 t A2 v A3; 9R:A3 v A4g and ABox = fR(I; J )g, and say we want abductive solutions for the observation fA4(I)g. If we apply the algorithm to this problem, three solutions are generated: fA1(J )g, fA2(J )g and fA3(J )g. If we allow expandable assertions, we get fA1 t A2(J )g and f9R:A3(I)g as solutions, but not f9R:A1(I)g or f9R:A2(I)g. These are closer to semantic minimality than f9R:A3(I)g.
Whether we manage to nd a way of generating all semantically minimal solutions, or just those attainable by allowing expandable assertions, we imagine that the user of a system implementing an abduction algorithm would want to be able to explore a range of such solutions.
The notion of semantic minimality is related to the notion of weakest su
cient conditions [
Algorithm 1 does not implement many of the optimizations (e.g. back-jumping
and caching) commonly used in DL tableau algorithms. Incorporating these into
our algorithm promises to give a real e ciency advantage over the FOL
connection tableau used in Klarman's algorithm [
This work also promises to be transferable to other more expressive DLs. As stated in Section 6.3, the problem of dealing with role assertions will disappear in languages that allow nominals.
Languages that do not have the nite model property will need some means of dealing with in nite models. (We imagine that the current assertion set at the point of blocking could simply be added to the set of models collected by extendedST so that it will be closed by all solutions.)
As stated in Section 6.4, we also intend to investigate the work on weakest su cient conditions and least common subsumers for their applicability to ranking solutions.
This work was partially funded by a European Union international research sta exchange scheme { Project number 247601, Net2: Network for Enabling Networked Knowledge, from the FP7-PEOPLE-2009-IRSES call. Thanks to Tommie Meyer of the CSIR Meraka Institute (in South Africa) and Enrico Franconi of the Free University of Bozen/Bolzano (in Italy) for infrastructure and support.