We develop an ABox abduction algorithm for description logics based on Reiter's minimal hitting set algorithm. It handles abduction problems with multiple observations and it supports the class of explanations allowing atomic and negated atomic concept and role assertions. As shorter explanations are preferred, the algorithm computes shorter explanations first and allows to limit their length. The algorithm is sound and complete for this class of explanations and for any given maximal length of explanations. In this paper we specifically focus on computing explanations for abduction problems with multiple observations, for which we explore two distinct approaches. The DL expressivity is limited only by the DL reasoner that our algorithm calls as a black box. We provide an implementation on top of Pellet, which is a full OWL 2 reasoner, so the expressivity is up to SROIQ. We evaluate the implementation on three different ontologies.
The goal of abduction [
On the other hand, general-purpose ABox abduction solvers, especially for more
expressive DLs are still underdeveloped. Some approaches are based on translation, e.g.,
Klarman et al. [
Building on ideas of Halland and Britz [
In this paper, we extend our previous results as follows: (a) we develop two distinct approaches for computing explanations for abduction problems with multiple explanations; (b) we incorporate a limitation on maximum length of explanations and improve effective exploration of the search space, starting from more desired (i.e., shorter) explanations; (c) we conduct preliminary empirical evaluation, specifically focusing on the comparison of the two multiple-observation approaches and on evaluation of the implemented optimization techniques. 2
For brevity we will only introduce the ALCHO DL [
A DL vocabulary consists of three countable mutually disjoint sets: set of individuals NI = ^a; b; §`, set of atomic concepts NC = ^A; B; §`, and set of roles NR = ^R; S; §`. Complex ALCHO concepts are recursively constructed as stated in Table 1, where C, D are ALCHO concepts, R, S are roles, and a, b are individuals. A TBox T is a finite set of GCIs and RIAs, and an ABox A is a finite set of concept, role or negated role assertions, as given in Table 1. A knowledge base is a pair K = .T ; A/. By the negation of any assertion ', i.e. ', we mean C.a/ for ' = C.a/, R.a; b/ for ' = R.a; b/, and R.a; b/ for ' = R.a; b/. Let A = ^' Ý ' Ë A` for any ABox A.
An interpretation of a knowledge base K is a pair I = . I ; I /, where I ^`, and I is an interpretation function s.t. aI Ë I for a Ë NI, AI Ó I for A Ë NC, and RI Ó I I for R Ë NR. Interpretation of complex concepts is inductively defined in Table 1. I satisfies an axiom ' (I ô ') as given in Table 1. I is a model of K if it satisfies all axioms included in K; K is consistent if there is a model I of K. A concept C is satisfiable w.r.t. K if there is a model I of K s.t. CI ^`. An axiom ' is entailed by K (K ô ') if for every model I of K it holds that I ô '. A set of axioms O is entailed by K (K ô O) if K ô ' for all ' Ë O.
Entailment and consistency checking are inter-reducible: e.g., for an ABox assertion
', K ô ' if and only if K ä ^'` is inconsistent. There is a number of DL reasoners
[
In DL we distinguish between TBox and ABox abduction [
Not all explanations are acceptable [
In this work we are interested in explanations in form of atomic and negated atomic ABox assertions. More specifically, we require E Ó ^A.a/; A.a/; R.a; b/; R.a; b/ Ý A Ë NC; R Ë NR; a; b Ë NI`. This class of explanations will be denoted AnRn. The subset of this class, which only contains explanatory, consistent, relevant, and minimal explanations will be denoted AnRnCER;sub.
Note that for any abduction problem P = .K; O/ both K and O are finite and the class of explanations is defined w.r.t. their finite combined signature, hence there is only finitely many explanations in either of these classes for any abduction problem P . 3
To compute explanations for single-observation abduction problems we build on our
previous work [
In order to find an explanation for an ABox abduction problem P = .K; O/ we need
to find a set of ABox assertions E such that K ä E ô O, i.e., such that K ä E ä ^O`
is inconsistent. This can be done by finding a hitting set [
To stay within the class AnRn we will rely on ABox encoding of models. ABox encoding of I is MI = ^C.a/ Ý I ô C.a/; CË ^A; A`; A Ë NC; a Ë NI` ä ^R.a; b/ Ý I ô R.a; b/; R Ë NR; a; b Ë NI` ä ^R.a; b/ Ý I ô R.a; b/; R Ë NR; a; b Ë NI`. Similarly as above, each K and O have a finite combined signature, hence each ABox encoding is finite. What is more, MI is not necessary homomorphic with the original model I; it ignores the anonymous part of the model (on purpose). Hereafter we automatically assume the ABox encoding whenever we talk about models.
According to Reiter [
Additional pruning conditions apply on the HS-tree [
Theorem 1. Given an ABox abduction problem P = .K; O/. Let M be a set of all models of K ä ^O` and let T = .V ; E; L/ be a pruned HS-tree for a collection of sets ^M Ý M Ë M`. Then ^H .n/ Ý n Ë V is a leaf in T that is not pruned` is the collection of all minimal explanations of P .
The Single Observation Abduction algorithm (SOA) is given in Algorithm 1. This
is a simplified and shortened pseudocode with some details omitted. For a more detailed
version please refer to our previous report [
The algorithm takes a knowledge base K and an observation O as first two inputs.
One improvement w.r.t. the previous work [
The last two parameters are auxiliary and they are only relevant when the algorithm is called as a subroutine to find explanations for multiple-observation abduction problems. In the single-observation case they will be set to O = ^O` and some new individual s0 (w.r.t. both K and O).
The algorithm first tries to obtain a model of K ä ^O` to use M as a label for the root node r. If there is none (i.e., K ô O) no (explanatory) explanations exist. Otherwise, successors of r are initialized and the tree is traversed breadth-first down to the depth l. For each node, we first evaluate H .n/. If it is inconsistent, irrelevant, or pruning applies, the node is pruned.
Next, if K ä ^O` ä H .n/ has a model, it is used to label n, otherwise we have found an explanation which is stored. Finally, after the desired depth l is fully traversed, all explanations are returned.
The algorithm calls the external solver (TA) on lines 1, 10, 11 and 15 though some TA calls can be saved thanks to model reuse. Also, while pruning ensures minimality, we have also filtered out all undesired explanations, hence the following result. Theorem 2. Let P = .K; O/ be a single-observation ABox abduction problem, l g 1, and s0 a new individual w.r.t. K and O. SOA(K; O; l; ^O`; s0) terminates, and it is sound and complete w.r.t. all explanations of P of the class AnRnCER;sub up to the length l.
In addition, if we remove the length limitation (i.e., we set l to Ø), the algorithm still terminates as the depth of the HS-tree is also bound by the number of possible ABox assertions. In such a case the algorithm finds all explanations of the input ABox abduction problem. 4
We now extend SOA to handle multiple observations. This algorithm is called ABox Abduction Algorithm (AAA). In fact, we explore two versions, one based on reducing the set of observations to a single observation (AAAR), the other based on splitting the multiple-observation problem into separate single-observation subproblems (AAAS). 4.1
An observation consisting of multiple concept assertions involving the same individual, say O = ^C1.a/; § ; Cn.a/`, can be easily reduced to an equivalent single observation O¨ = C1 à 5 à Cn.a/. Cases involving multiple individuals or even role assertions are less straightforward, but in DLs featuring nominals they may be encoded as follows. Lemma 1. Let P = .K; O/ be a multiple-observation ABox abduction problem with O = ^C1.a1/; § ; Cn.an/; R1.b1; c1/; § ; Rm.bm; cm/; Q1.d1; e1/; § ; Ql.dl; el/`, where C are concepts, Ri; Qj Ë NR and ai; bj ; cj ; dk; ek Ë NI for i Ë [1; n], j Ë [1; m], i k Ë [1; l]. Let E Ó ^A.a/; A.a/; R.a; b/; R.a; b/ Ý A Ë NC; R Ë NR; a; b Ë NI`. Let P ¨ = .K; O¨/ be a single-observation ABox abduction problem with O¨ = X.s0/, s.t. s0 is new w.r.t. K, O, and E , and
X =.^a1` á C1/ à 5 à .^an` á Cn/ à .^b1` á ÇR1:^c1`/ à 5 à .^bm` á ÇRm:^cm`/ à .^d1` á ÅQ1:^e1`/ à 5 à .^dl` á ÅQl:^el`/ : Then E is an explanation of P if and only if it is an explanation of P ¨.
Notice that the lemma rules out explanations involving the individual s0 introduced during the reduction. If this is not the case P ¨ may indeed have more explanations than P . These unwanted explanations need to be filtered out.
Example 1. Let K = ^A Þ B; C Þ D`, and O = ^B.a/; D.b/`. The only explanation of P = .K; O/ is E1 = ^A.a/; C.b/`. Using the reduction we obtain P ¨ = .K; O¨/ with O¨ = .^a` á B/ à .^b` á D/.s0/. However, besides for E1 which is an explanation of P ¨ courtesy of Lemma 1, in addition E2 = ^A.s0/; C.s0/`, E3 = ^A.a/; C.s0/`, and E4 = ^A.s0/; C.b/` are explanations of P ¨.
The AAAR algorithm is listed in Algorithm 2. It takes a knowledge base K, a set of observations O, and a length upper bound l g 1 as inputs. It reduces the set O to a single observation O¨ according to Lemma 1 and passes the reduced single-observation abduction problem to SOA.
Algorithm 2 AAAR (K,O,l): AAA based on Reduction Require: knowledge base K, set of observations O = ^C1.a1/; § ; Cn.an/; R1.b1; c1/; § ;
Rm.bm; cm/;Q1.d1; e1/; § ;Ql.dl; el/`, max length of an explanation l Ensure: set SE of all explanations of P = .K; O/ of the class AnRnCER;sub up to the length l 1: s0 } new individual w.r.t. K and O 2: X } .^a1` á C1/ à 5 à .^an` á Cn/ à .^b1` á ÇR1:^c1`/ à 5 à .^bm` á ÇRm:^cm`/ à .^d1` á ÅQ1:^e1`/ à 5 à .^dl` á ÅQl:^el`/ 3: O¨ } X.s0/ 4: SE } SOA(K; O¨; l; O; s0)
Instead of filtering the unwanted explanation involving the auxiliary individual s0 ex post, AAAR passes s0 to SOA as the fifth parameter. SOA then excludes the assertions involving s0 already from the models returned by TA, reducing the HS-tree.
Since for multiple-observation abduction the relevance needs to be checked w.r.t. all observations AAAR also passes the original set of observations O to SOA as the fourth parameter. Observing that SOA handles the auxiliary parameters correctly, the correctness of AAAR is then a consequence of the correctness of SOA. Theorem 3. Let P = .K; O/ be a multiple-observation ABox abduction problem, and let l g 1. Then AAAR (K,O,l) terminates, and it is sound and complete w.r.t. all explanations of P of the class AnRnCER;sub up to the length l.
As for SOA, if we remove the depth limitation, the algorithm finds all explanations of the input ABox abduction problem. 4.2
A multiple-observation abduction problem may also be solved by splitting P into n
subproblems Pi = .Ki; Oi/ and answering each Pi separately using SOA. If there is no
bound on length, this is quite easy: we simply combine the results in terms of union
with some additional filtering [
AAAS algorithm is listed in Algorithm 3. It receives a knowledge base K, observations O = ^O1; § ; On`, and a length upper bound l g 1 as inputs.
The algorithm initializes an empty collection which will be used to accumulate the partial results returned by SOA and a dummy new individual s0 (lines 1–2).
We cannot just directly use K in each subproblem Pi, as we may miss explanations involving individuals from other observations. Hence K¨ is used, obtained by adding ñ.a/ into K for all such individuals a (line 3).
The algorithm then loops through Oi Ë O (lines 4–11) and calls SOA for K¨, Oi and l. We also pass the set of observations O (due to relevance checks) and a dummy new individual s0 to SOA as auxiliary parameters. If one of the observations cannot be explained (SOA returned ^`) then neither the whole set O can be explained (line 7).
Observe that O and O ä ^Oi Ë O Ý K ô O ` have the same set of explanations. i Therefore if SOA returned "nothing to explain" for some Oi the result is simply excluded from . If this happens for all Oi Ë O, the overall result is "nothing to explain".
If is non-empty the explanations of P are computed as unions E1 ä 5 ä Em, combining all possible Ei from each SEi Ë with the others (line 15). While SOA already did some filtering of the partial results, supersets, irrelevance, and inconsistence may have been introduced by unifying them, hence they are filtered out (line 16).
Finally, also AAAS is correct up to any length l. And if the length limitation is removed, the algorithm finds all explanations of the input ABox abduction problem. Theorem 4. Let P = .K; O/ be a multiple-observation ABox abduction problem, and let l g 1. Then AAAS (K,O,l) terminates, and it is sound and complete w.r.t. all explanations of P of the class AnRnCER;sub up to the length l. 5
We have implemented the ABox abduction algorithm into the AAA solver. For
implementation details, see our previous report [
We have chosen three ontologies for the evaluation: Family ontology (our own small
ontology of family relations)1, Coffee ontology by Carlos Mendes2, and LUBM (Lehigh
University Benchmark [
On each input we ran AAA iteratively, rising maximal explanation length (i.e. the maximal depth of the HS-tree). The following properties were recorded from each run: time of execution, number of explanations, number of the nodes in the HS-tree, number of TA calls, number of reused models, number of pruned nodes.
Apart from exceptional cases all experiments were repeated 10 times on the same input and the results were averaged. All experiments were executed both allowing and disallowing loops (i.e., reflexive role assertions) in explanations. For the lack of space 1 http://dai.fmph.uniba.sk/~pukancova/aaa/ont/ 2 https://gist.githubcom/cmendesce/56e1e16aee5a556a186f512eda8dabf3 we report only the former in this paper. On average, the experiments with loops took 243.24 % more time and found 26.99 % more explanations.
All experiments were done on a 6-core 3.2 GHz AMD Phenom™ II X6 1090T Processor, 8 GB RAM, running Ubuntu 17.10, Linux 4.13.0, while the maximum Java heap size was set to 4GB. We have used the GNU time utility to measure the CPU time consumed by AAA while running in user mode, summed over all threads. The algorithm was executed once on each ontology with a specifically chosen observation set, each consisting of three assertions: ^Father.jack/; Mother.eva/; Person.f red/` for Family ontology, ^Milk.a/; Cof f ee.b/; Pure.c/` for Coffee ontology, ^Person.jack/; Employee.jack/; Publication.a/` for LUBM. The aim was to compare the reduction (R) and the splitting (S) approach therefore all experiments were run with either option.
The experiment was processed up to the depth 3, as even in this depth the algorithm ran out of memory in half of the cases. The reason for this is that the observations contain multiple individuals which increases the search space. Most runs were repeated 10 times, with four exceptions: LUBM (R and S), depth 3 and Coffee (R), depth 3 as these runs ran out of memory; and Coffee (S) as the execution time was too high.
In Figure 1 the execution times for each ontology and both approaches are plotted. These times are also stated in Table 3 with the numbers of the computed explanations in each experiment. The out-of-memory cases show the time when the memory was exceeded. The average deviation in time between runs was 2.66 % for the splitting approach and 1.6 % for the reduction approach.
LUBM (S) LUBM (R) Coffee (S) Coffee (R) Family (S)
Family (R) 1 2
3
For each run of the algorithm, a number of pruned nodes, reused models and TA calls was recorded. In Figure 2 a proportion of these numbers for each experiment is plotted (for depths for which memory was not exceeded).
The execution time is always higher for the splitting approach than for the reduction approach (ignoring the out-of-memory cases). Indeed this is because in the splitting approach the length limit is applied to each subproblem separately. Thus, also some explanations longer than the limit are computed (as unions of the separate results obtained for each subproblem).
From one point of view, the reduction approach is more efficient, as for a length limit l it always assures all the explanations up to l, and in our experiments it always reached lower time than the splitting approach for the same limit l.
On the other hand, we observed that the splitting approach may often find higher numbers of explanations much more quickly, e.g. in Table 3 (Family ontology). AAAR found all 9 explanations up to length 3 in 79.68 seconds. AAAS found 7 of these in 4.54 seconds (after depth 1) and it already found 144 explanations in 21.78 seconds (after depth 2). In fact, it took slightly longer to run it to depth 3 (19.48 minutes) but during this time it found the 9 explanations up to the length 3 together with additional 804 longer explanations. Though we cannot characterize this additional explanations in any way (apart from being sound), this approach may be suitable for some applications, where completeness is not a high priority, and the main goal is to compute as much explanations as possible. 6
We have described a sound and complete ABox abduction algorithm that handles
multiple observations, and supports the class of explanations including atomic and negated
atomic concept and role assertions. Unlike the previous works which can only support
(or are complete up to) limited DL expressivity [
In this paper we have predominantly focused on extending our algorithm and
implementation to handle multiple-observation abduction problems. We have developed and
evaluated two distinct approaches. Our evaluation shows applicability of the approach,
particularly when looking for explanations of lower lengths (i.e. those most preferred)
and with a smaller number of involved individuals. The evaluation also shows how the
implemented optimization techniques are essential in reducing the search space. Note
that this is only our first attempt at an implementation, in the future we would like to
plug in and compare different reasoners, but also to explore possible improvements in
the MHS algorithm [
Acknowledgments. This work was supported by the Slovak national project VEGA 1/0778/18. Júlia Pukancová is also supported by an extraordinary scholarship awarded by Faculty of Mathematics, Physics, and Informatics, Comenius University in Bratislava, and by the Comenius University grant no. UK/266/2018. We would like to thank to anonymous reviewers from previous DL workshops for valuable suggestions.