=Paper=
{{Paper
|id=Vol-1193/paper_42
|storemode=property
|title=TBox Abduction in ALC Using a DL Tableau
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_42.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/HallandBK14
}}
==TBox Abduction in ALC Using a DL Tableau==
https://ceur-ws.org/Vol-1193/paper_42.pdf
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)