Tableau-Based ABox Abduction for the ALCHO Description Logic

Abstract

Abduction is a useful decision problem that is related to diagnostics. Given some observation in form of a set of axioms, that is not entailed by a knowledge base, we are looking for explanations, sets of axioms, that can be added to the knowledge base in order to entail the observation. ABox abduction limits both observations and explanations to ABox assertions. In this work we focus on direct tableau-based approach to answer ABox abduction. We develop an ABox abduction algorithm for the ALCHO DL, that is based on Reiter's minimal hitting set algorithm. We focus on the class of explanations allowing atomic and negated atomic concept assertions, role assertions, and negated role assertions. The algorithm is sound and complete for this class. The algorithm was also implemented, on top of the Pellet reasoner.

Keywords

• Description logics
• ABox abduction
• implementation

-

Abductive reasoning [ 11 ] focuses on deriving explanations. Given a knowledge base K and an observation O that is not entailed (i.e., K 6j= O) we are looking for an explanation E that, when added to K, would allow to entail O (i.e., K [ E j= O). From the DL perspective, we distinguish between TBox abduction, where both E and O are limited to TBox axioms, and ABox abduction, where they are limited to ABox assertions [ 3 ]. While TBox abduction may be used, e.g., in ontology engineering, ABox abduction found uses in diagnostic reasoning [ 8, 13, 3 ], or tasks such as multimedia interpretation [ 12 ]. In our research we focus on the latter problem.

Compared to the approaches based on translations to di erent formalisms [ 10, 2 ], Halland and Britz [ 5, 4 ] propose a direct tableau-based approach built on top of Reiter's minimal hitting set algorithm [ 15 ]. This method avoids the translation overhead, and may also build on the existing tableau optimization techniques for DLs which have been intensively studied [ 17 ].

In our previous paper [ 14 ], we have extended the approach of Halland and Britz, and we have provided an implementation on top of the Pellet reasoner [ 16 ]. In this paper, we have further extended this work: we lifted the algorithm to the ALCHO DL; we have enabled support for multiple observations in form of any ABox assertions; we have also extended the explanations to include role assertions and negated role assertions; and we have proven soundness and completeness w.r.t. this class of observations and explanations. 2

ABox Abduction in DL

We build on top of the ALCHO DL [ 1 ]. A DL vocabulary consists of countably in nite mutually disjoint sets of individuals NI, roles NR, and atomic concepts NC. Concepts are recursively built using constructors :, u, 9, fag, as shown in Table 1. Additional concepts union (C t D := :(:C u :D)) and value restriction (8R:C := :9R::C) are de ned as syntactic sugar; and also ::C := C by de nition.

A knowledge base K = (T ; A) consists of a TBox T and an ABox A. A TBox is a nite set of GCI and RIA axioms of the form C v D and R v S, where C; D are concepts and R; S 2 NR. An ABox is a nite set of concept assertions of the form C(a), and role assertions of the form R(a; b), where a; b 2 NI, C is a concept, and R 2 NR.

An interpretation is a pair I = ( I ; I ), where I 6= ; is a domain, and the interpretation function I maps each individual a 2 NI to aI 2 I , each atomic concept A 2 NC to AI I , each role R 2 NR to RI I I in such a way that the constraints on the left-hand side of Table 1 are satis ed.

An interpretation I satis es an axiom ' (denoted I j= ') if the respective constraint in Table 1 is satis ed. It is a model of a knowledge base K = (T ; A) (denoted I j= K) if I j= ' for all ' 2 T [ A. A knowledge base is consistent, if there is at least one interpretation I such that I j= K. A knowledge base entails an axiom ' (denoted K j= ') if I j= ' for each I j= K.

We de ne :' = :C(a) for a concept assertion ' = C(a). Thanks to presence of nominals in ALCHO [ 7, 5 ] we are also able to de ne :' = :R(a; b) := 8R:fbg(a) for a role assertion ' = R(a; b), and :' := R(a; b) for ' = :R(a; b). In addition, :A = f:' j ' 2 Ag for any set of ABox assertions A.

In ABox abduction, we are given a knowledge base K and an observation O consisting of ABox assertions, that is, some evidence we have observed. The task is to nd an explanation E , again, consisting of ABox assertions, such that K [ E j= O. De nition 1 (ABox Abduction Problem [ 3 ]). An ABox abduction problem is a pair P = (K; O) such that K is a knowledge base in DL and O is a set of ABox assertions. A solution of P (also called explanation) is any nite set E of ABox assertions such that K [ E j= O.

Example 1. Consider the ABox abduction problem P = (K; O), where knowledge base K has two axioms:

Professor t Scientist v Academician

AssocProfessor v Professor

(1) (2) and we observe O = fAcademician(jack)g, while K 6j= O. There is a number of explanations Ei s.t. K [ Ei j= O, e.g. E1 = fProfessor(jack)g, E2 = fScientist(jack)g, E3 = fProfessor(jack); Scientist(jack)g, E4 = fAssocProfessor(jack)g, and even E5 = fAcademician(jack)g.

While De nition 1 establishes the basic reasoning mechanism of abduction, some of the explanations it permits are clearly undesired. The explanations should, at minimum, ful l some basic sanity requirements.

De nition 2 ([ 3 ]). Given an ABox abduction problem P = (K; O) and its solution E we say that: 1. E is consistent if E [ K 6j= ?, i.e. E is consistent w.r.t. K; 2. E is relevant if E 6j= O, i.e. E does not entail O; 3. E is explanatory if K 6j= O, i.e. K does not entail O.

An explanation should be consistent, as anything follows from inconsistency; and so, an explanation that makes K inconsistent does not really explain the observation. It should be relevant { it should not imply the observation directly without requiring the knowledge base K at all. And it should be explanatory, that is, we should not be able to explain the observation without it. Example 2. Consider the ABox abduction problem P = (K; O) and its solutions E1; : : : ; E5 from Example 1. The explanations E1; : : : ; E4 are consistent, relevant, and explanatory. However, E5 = fAcademician(jack)g is not relevant, since E5 j= O.

Hereafter, when we say explanation we always mean a consistent, relevant, and explanatory explanation, unless indicated otherwise. Subsequently we can think about further requirements to eliminate undesired explanations. Usually it is clear that we want to explain observations only with su cient assumptions and not to hypothesize too much. Therefore syntactic minimality is de ned. De nition 3 (Syntactic Minimality). Assume an ABox abduction problem P = (K; O). Given two solutions E and E 0 of P, we say that E is (syntactically) smaller than E 0 if E E 0.1 We further say that a solution E of P is syntactically minimal if there is no other solution E 0 of P that is smaller than E . Example 3. Consider the ABox abduction problem P = (K; O) from Example 2. Four explanatory, consistent, and relevant explanations were found. We may observe that E1 = fProfessor(jack)g and E2 = fScientist(jack)g are both smaller than E3 = fProfessor(jack); Scientist(jack)g, i.e. E1 E3 and E2 E3. Therefore E3 is not a syntactically minimal explanation, while the other three are. 3

Our Approach

Based on Reiter's work [ 15 ], on the proposal of Halland and Britz [ 5, 4 ], and on our previous works [ 13, 14 ] we de ne an ABox abduction algorithm for ALCHO.

For a single observation O, a solution of an abduction problem P = (K; O) according to De nition 1 can be obtained as any E s.t. K[E [f:Og is inconsistent (due to reducibility of entailment into consistency checking [ 1 ]). As showed by Reiter [ 15 ], we can compute the minimal explanations of P by nding all minimal hitting sets for all models of K [ f:Og.

De nition 4 (Minimal Hitting Set [ 15, 9 ]). A hitting set for a collection of sets F is a set H s.t. H \ S 6= fg for every S 2 F . A hitting set H for F is minimal if there is no other hitting set for F s.t. H0 ( H.

De nition 5 (HS-Tree [ 15 ]). A HS-tree for F is T = (V; E; L; H), where (V; E) is a minimal tree in which the labelling function L labels the nodes of V by elements of F , the edges of E by elements of sets in F , and H(n) is the set of edge-labels from the root node to n 2 V , s.t.: (a) for the root r 2 V : L(r) = S for some S 2 F , if F 6= fg, otherwise L(r) = fg; (b) for each n 2 V : L(n) = S for some S 2 F s.t. S \ H(n) = fg, if such S 2 F exists, otherwise L(n) = fg; (c) each n 2 V has a successor n for each 2 L(n) with L(n; n ) = .

A HS-tree T for F contains all minimal hitting sets but it may contain some other hitting sets. For sake of optimization Reiter [ 15 ] proposed to construct HStree by breadth- rst search and to prune it as follows: a node n 2 V is pruned if there is n0 2 V s.t.: (a) either H(n0) H(n) and L(n0) = fg (i.e., H(n) is not minimal because its subset H(n0) is also a hitting set); (b) or H(n0) = H(n) and L(n0) = S 2 F (i.e., both paths are equivalent therefore we can prune one of them). A pruned HS-tree is obtained from a HS-tree by removing all pruned nodes including their descendants.

Theorem 1 (Reiter [ 15 ]). Let T = (V; E; L; H) be a pruned HS-tree for a collection of sets F . Then fH(n) j n 2 V , L(n) = fg, and n is not prunedg is the collection of all minimal hitting sets for F . 1 Note that before we compare two solutions E and E0 of P syntactically, we typically normalize the assertions w.r.t. (outermost) concept conjunction: as C u D(a) is equivalent to the pair of assertions C(a) and D(a), we replace the former form by the latter while possible.

Single Concept Observation The algorithm is given in Algorithm 1. It starts by calling the tableau algorithm (TA) on K0 = K [ f:Og. If there is no model, the observation already follows from K { there is nothing to explain. If there is a model I, we extract all atomic and negated atomic concept assertions from it into M = fC(a) j I j= C(a); C 2 fA; :Ag; A 2 NC; a 2 NIg, and store this representation of M for later reuse (lines 1{6). Note, hereafter whenever we refer to a model M we mean this representation of it.

A new HS-tree T = (V; E; L; H ) is then initialized with root r 2 V , labelled by :M . And, a successor node is added to V for each 2 :M , together with a respective edge labelled by (lines 7{9).

The root node r is now fully processed. We initialize the output set of explanations as SE = fg and traverse the remaining nodes in V by breadth- rst search (lines 10{30).

For each such node n, we rst evaluate H(n) and check if pruning can be applied: if there is a clash within H(n), or if some S H(n) is already in SE , or there is some n0 2 V such that H(n0) = H(n), we are not interested in H(n) and so we label n by fg (lines 13{14).

If none of this is the case, we try to nd a model of K0 [ H(n). We rst try to reuse a suitable model M which was previously computed (line 16). If there is none, we call TA on K0 [ H(n). If we obtain a model I we compute its representation M and store it for later reuse (lines 18{20). We then label n by :M and initialize its successors and respective edge-labels similarly as for the root node (lines 27{29).

If no model was returned by TA, then H(n) is a candidate explanation: we add it to SE , if it is consistent and relevant. In this case n is also labelled by fg (lines 21{24).

Once we traversed all nodes in T a minimal HS-tree is constructed and SE contains all minimal explanations (line 30). 3.2

Role Assertions We will now describe how Algorithm 1 is extended to allow also role assertions, including negated, as the observation and also in the explanations. The case of the observation is trivial thanks to the choice of DL with nominals: we can simply permit the observation O on the input to be also in the form R(a; b) or :R(a; b) for R 2 NR, a; b 2 NI. This only a ects line 1 where :O is computed as given in Section 2.

In order to include role assertions also in the explanations we need to modify the construction of the model M which was previously described in Section 3.1. Given the model I returned by the TA, we rede ne its representation M as: M = fC(a) j I j= C(a); C 2 fA; :Ag; A 2 NC; a 2 NIg [ fR(a; b) j I j= R(a; b); R 2 NR; a; b 2 NIg [ f:R(a; b) j I j= :R(a; b); R 2 NR; a; b 2 NIg : (3)

Algorithm 1 SOA(K,O): Single Observation Abduction

Input: knowledge base K, observation O Output: set of all explanations SE 1: K0 K [ f:Og 2: M call TA with input K0 3: if M = fg then 4: return "nothing to explain" 5: end if 6: MS fM g 7: create new HS-tree T = (V; E; L; H) with root r 8: L(r) :M 9: for each . TA returns a model of K0 2 :M create a successor n of r and label the resp. edge by . H(n) { set of edge-labels on path r{n The rst part involving concept assertions is unchanged, plus we also add all role assertions and negated role assertions that hold in I. Note, from now on, whenever we talk about model M we mean the representation in this form. The actual extraction of the models from TA is described below in Section 5.

Example 4. Consider the knowledge base K:

SlovakScientist v 9livesIn:fslovakiag coauthors v workWith

(4) (5) Given the observation O1 = flivesIn(jack; slovakia)g and the ABox abduction problem P1 = (K; O1) we are able to nd one consistent, relevant, explanatory, and subset minimal explanation E1 = fSlovakScientist(jack)g of P1, i.e., K [ E1 j= O1. Similarly, given the observation O2 = fworkWith(jack; mary)g, E2 = fcoauthors(jack; mary)g is an explanation of P2 = (K; O2), i.e., K[E2 j= O2. 3.3

Multiple Observations Consider the abduction problem P = (K; O) with a set of observations O = fO1; : : : ; Ong. The problem P can be simply split into n subproblems P1 = (K; O1), . . . , Pn = (K; On). Observe that if K [ Ei j= Oi for 1 i n, then E = E1 [ : : : [ En is an explanation of P, i.e., K [ E j= O.

Hence, in order to compute all explanations for P = (K; O) we need to compute all combinations from explanations of every observation Oi. The algorithm is described more precisely in Algorithm 2.

Example 5. Consider the knowledge base K from the Example 4 and the observation O = flivesIn(jack; slovakia); workWith(jack; mary)g. We are looking for E s.t. K [ E j= O. We split P = (K; O) into two subproblems, where P1 = (K; O1), O1 = flivesIn(jack; slovakia)g and P2 = (K; O2), O2 = fworkWith(jack; mary)g. Actually, P1 and P2 are already solved in Example 4; the set of all explanations for O1 is SE1 = fE1g and for O2 is SE2 = fE2g. In this very simple example, SEmin = fE1 [ E2g and so the only solution of P is E = fSlovakScientist(jack); coauthors(jack; mary)g.

Note that there are some special cases the algorithm needs to observe. Firstly, if there is no explanation Ei that explains Pi for at least one i, then there is also no explanation that explains P (lines 4{5).

Secondly, if K j= Oi then Pi does not contribute to E , as given more precisely in Observation 1.

Observation 1. Given a set of observations O = fO1; : : : ; Ong and given O0 = O n fOi 2 O j K j= Oig, we have K [ E j= O if and only if K [ E j= O0. Hence P = (K; O) has the same set of explanations as P = (K; O0).

The algorithm uses the set to collect explanations only for Oi 2 O0 (lines 6{7).

Thirdly, even if the explanation Ei of Pi is minimal (consistent and relevant) for all 1 i n, it is not guaranteed that E = E1 [ : : : [ En is minimal, consistent and relevant. Therefore we need to lter out the undesired explanations additionally (line 14). 4

Soundness and Completeness

Lemma 1. Let K be an ALCHO knowledge base and let O be an observation in form of an ALCHO ABox assertion. Let SE be the output of the SOA algorithm initialized with K and O on the input. Then each E 2 SE is a consistent, relevant, explanatory, and subset minimal explanation of the abduction problem P = (K; O).

Algorithm 2 AAA(K,O): ABox Abductive Algorithm

fE1 [ : : : [ Em j Ei 2 SEi ; SEi 2 ; m = j jg

fE j E 2 SE and 8E0 2 SE : E0 6 E and E is consistent and relevantg

SE expl. 14: SEmin 15: end if 16: return SEmin Proof. If SOA returned "nothing to explain", it terminated in line 4, and this was because K [ f:Og was inconsistent, which is the same as K j= O, and in such a case there are no explanations.

In the other case SOA returned a set SE . Let E 2 SE . In such a case E = H(n) for some node n and it was added to SE on line 23. However in this case we have also called TA on K [ f:Og [ E on line 18 and it returned no model (as we tested on line 19). Hence K [ E j= O, i.e., E is an explanation of P.

In addition, E is consistent and relevant, because we have tested this (on line 22) immediately before adding it to SE . It is also explanatory because in the other case the algorithm returned "nothing to explain" and terminated already on line 4 as described above.

The minimality of E follows from the fact that we only add such E = H(n) into SE on line 23 which correspond to paths from root to a leaf which are not pruned in the HS-tree, and as showed by Reiter [ 15 ], in a pruned HS-tree all such paths correspond to minimal hitting sets. This can be veri ed by observing the HS-tree is constructed breadth- rst, that is, when E = H(n) is considered as an explanation, all smaller explanations are already stored in SE . Consequently if some S H(n) was previously found, the if-condition on line 13 is evaluated as true and hence the assignment of E into SE on line 23 is not executed. Theorem 2 (Soundness). Let K be an ALCHO knowledge base and let O be a set of observations in form of ALCHO ABox assertions. Let SE be the output of the AAA algorithm initialized with K and O on the input. Then each E 2 SE is a consistent, relevant, explanatory, and subset minimal explanation of the abduction problem P = (K; O). Proof. If AAA returned "nothing to explain", it was because on line 10 collection of the sets of all explanations was empty. This can only be the case when SOA returned "nothing to explain" for each Oi (line 6), that is, according to Observation 1, O0 = fg. This means that K j= Oi for each Oi, and so K j= O.

In the other case AAA returned a set SE . Let E 2 SE . From lines 13{14 it is apparent that E = E1 [ : : : [ Em where Ei 2 SEi and each SEi 2 is the set of minimal explanations for Oi returned by SOA on line 3.

From Lemma 1 we have K [ Ei j= Oi for all Ei 2 SEi . Observe, that collects SEi for all those Oi, for which K 6j= Oi (lines 6{7), hence from Observation 1 we have K [ E j= O, that is E is an explanation of P = (K; O). Moreover, subset minimality, consistency, and relevancy of each E 2 SE is consecutively veri ed on line 14. E is also explanatory, as otherwise K j= O, i.e., K j= Oi for all i, and thus = fg. In such a case the algorithm already terminates on line 11. Lemma 2. Let K be an ALCHO knowledge base and let O be an observation in form of an ALCHO ABox assertion. Let E fA(a); :A(a); R(a; b); :R(a; b) j A 2 NC; R 2 NR; a; b 2 NIg be a consistent, relevant, explanatory, and subset minimal explanation of the abduction problem P = (K; O). Then the SOA algorithm, initialized with K and O on the input, produces E as one of its outputs. Proof. Given an abduction problem P = (K; O), let SE be an output of SOA for P. Let E be a consistent, relevant, explanatory, and subset minimal explanation of P.

As E is explanatory, K [ f:Og has at least one model. Hence the root r of HS-tree T constructed by SOA is labelled by :M , where M is a model of K [ f:Og (line 8). Note that, from the construction of M (3) it follows that ' 2 :M or :' 2 :M for every atomic ABox assertion '.

It is clear that K [ M [ f:Og is consistent and so E 6 M , i.e. there is an ABox assertion 1 2 E s.t. 1 62 M . Hence : 1 2 M , and so 1 2 :M , and also L(r; n 1 ) = 1 for some successor n 1 of r, from line 9.

The rest of the proof is by induction. Let us assume that SOA extended T until there is a node n k s.t. H(n k ) E and jH(n k )j = k. We will show that ( ) either H(n k ) = E or there is some k+1 2 E n H(n k ) which will become the label of some new edge leading from n k . Observe that none of the pruning conditions applies on n k : E is consistent, and hence H(n k ) does not contain a clash; no S ( H(n k ) was previously added into SE because E is minimal; and if there is some other node n in T such that H(n) = H(n k ) we can assume w.l.o.g. that n k is the one which is visited rst and hence it is not pruned. Next we distinguish between two cases. In the rst case K[H(n k )[f:Og is inconsistent, and so H(n k ) = E, L(n k ) = fg and therefore SOA adds H(n k ) = E into SE . In the second case K [ H(n k ) [ f:Og is consistent, i.e. it has a model Mk and L(n k ) = :Mk. It is clear that H(n k ) Mk and that K [ Mk [ f:Og is consistent and so E 6 Mk, i.e. there is k+1 2 E n H(n k ) s.t. k+1 62 Mk, and so k+1 2 :Mk. Therefore SOA consequently creates a node n k+1 with L(n k ; n k+1 ) = k+1.

Since we have proved ( ) for any k, by induction SOA will eventually create a node n m s.t. H(n m ) = E and L(n m ) = fg. That means that SOA has added H(n m ) = E into SE .

Theorem 3 (Completeness). Let K be an ALCHO knowledge base and let O be an observation set of ALCHO ABox assertions. Let E fA(a); :A(a); R(a; b); :R(a; b) j A 2 NC; R 2 NR; a; b 2 NIg be a consistent, relevant, explanatory, and subset minimal explanation of the abduction problem P = (K; O). Then the AAA algorithm, initialized with K and O on the input, produces E as one of its outputs.

Proof. Given an abduction problem P = (K; O), let SEmin be the output of AAA for P. Let E be a consistent, relevant, explanatory, and subset minimal explanation of P.

As K [ E j= O = fO1; : : : ; Ong, then also K [ E j= Oi and hence E explains each Pi = (K; Oi).

Let Ei be a smallest subset of E that explains Pi. For some i's Ei may equal to fg but not for all, as then K j= O which is not the case. If Ei 6= fg then Ei is a minimal explanation of Pi, otherwise it would not be a smallest subset of E that explains Pi. It is trivially explanatory, and it is also consistent and relevant w.r.t. Pi (because whole E is). In addition E = E1 [ [ En because E1 [ [ En explains all O1; : : : ; On hence otherwise E would not be minimal.

Now, AAA called SOA and obtained the set of explanations SEi for each Pi. From Lemma 2 we have that SEi contains all minimal, consistent, relevant, and explanatory explanations of Pi. Hence on line 13 E was surely added into SEi . But since E is minimal, consistent, relevant, and explanatory, it was also added to SEmin on line 14.

5 Implementation

Our algorithm is implemented in Java. It is based on our previous implementation that is extended with more forms of observations and explanations. As described in our previous work [ 14 ], knowledge base consistency is veri ed by the Pellet reasoner [ 16 ] (version 2.3.1). Pellet is an optimized tableau-based reasoner, that will enable to involve optimizations such as incremental reasoning in our implementation in the future. The run of our algorithm corresponds to Algorithm 2.

OWL ontology and the set of ABox assertions representing the observations are loaded as input and consequently processed into Pellet knowledge base K. Firstly, Pellet decides a consistency of K. After a successful consistency check, we obtain the ABox A corresponding to the model of K using the getABox() method and construct M as described in Section 3.2. For each node a we extract from A all atomic concepts in its label and all outgoing edges (using the getTypes() and getOutEdges() methods), and we add the corresponding ABox assertions to M . Consequently, we compute the completion of M by adding the negation of all atomic assertions which are not already in M .

Our implementation uses Pellet for consistency checking and for model construction. All other features, from initializing AAA algorithm through constructing the HS-tree to answering the set of all minimal hitting sets for the input set of observations, are executed by our own implementation. All optimizations presented in this paper, such as HS-tree pruning or model reusing, are implemented.

Our implementation is available for download at: http://dai.fmph.uniba. sk/~pukancova/aaa/ . 6

Conclusions

We have described an ABox abduction algorithm for the ALCHO DL, which is based on Reiter's work on minimal hitting sets [ 15 ]. The algorithm calls a DL reasoner as a black box; the current approach is tableau-based as we rely on Pellet reasoner.

Our algorithm permits a set of any ABox assertions (including negated role assertions) as the observation, and computes explanations constrained to minimal sets of atomic and negated atomic ABox assertions. Our work extends the works of Halland and Britz [ 5, 4 ] in the following respects: (a) permitting ALCHO instead of ALC; (b) computing models on the y, during the search for explanations, instead of during pre-processing; (c) formally establishing both soundness and completeness for the given class of observations and explanations; and (d) developing also an implementation built on top of the Pellet [ 16 ] reasoner. Compared to our previous work [ 14 ], we have extended the algorithm as well as the implementation to handle multiple observations and to permit role assertions in both observations and explanations, and we have established soundness and completeness.

Regarding the complexity, ALCHO is ExpTime-complete [ 6 ], and Reiter's minimal hitting set algorithm is NP-complete [ 15, 9 ], so the combined overall complexity of our algorithm is still ExpTime. In the future, we also plan to further optimize the implementation of our algorithm, especially by exploiting incremental reasoning that is partly available in Pellet 2.3.1. Pellet enables to reuse the previously built tableau structures in cases when assertions are added to the ABox, however it is not able to handle deletions. We plan to exploit techniques similar to tableau caching to deal with the latter problem.

In the future, we would like to consider also semantically minimal explanations [ 14 ]. In our opinion, this notion of minimality is highly relevant for practical problems. We also want to focus on explanations involving complex concept assertions, and anonymous individuals, as there are some speci c abduction problems where such explanations are interesting. This could be di cult because of the possibility of in nitely many solutions. It is necessary to specify the concrete target forms of these explanations and to propose new form of model representations including also complex concept assertion. As the complexity of the algorithm will increase, we need to analyse also other possible optimizations. Acknoledgements. We would like to thank to the anonymous reviewers for a number of fruitful comments.

References

1. Baader , F. , Calvanese , D. , McGuinness , D.L. , Nardi , D. , Patel-Schneider , P.F . (eds.): The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press ( 2003 )

2. Du , J. , Qi , G. , Shen , Y. , Pan , J.Z. : Towards practical ABox abduction in large description logic ontologies . Int. J. Semantic Web Inf. Syst . 8 ( 2 ), 1 { 33 ( 2012 )

3. Elsenbroich , C. , Kutz , O. , Sattler , U. : A case for abductive reasoning over ontologies . In: Proceedings of the OWLED*06 Workshop on OWL: Experiences and Directions , Athens, Georgia, USA, November 10 - 11 , 2006 ( 2006 )

4. Halland , K. , Britz , K. : Abox abduction in ALC using a DL tableau . In: 2012 South African Institute of Computer Scientists and Information Technologists Conference, SAICSIT '12, Pretoria , South Africa, October 1-3 , 2012 . pp. 51 { 58 ( 2012 )

5. Halland , K. , Britz , K. : Nave ABox abduction in ALC using a DL tableau . In: Proceedings of the 2012 International Workshop on Description Logics, DL-2012 , Rome, Italy, June 7-10, 2012 . Sun SITE Central Europe (CEUR) ( 2012 )

6. Hladik , J. , Model , J.: Tableau systems for SHIO and SHIQ . In: Haarslev, V. , Moller, R. (eds.) Proc. of the 17th Int. Workshop on Description Logics (DL 2004 ). CEUR Workshop Proceedings , vol. 104 , pp. 168 { 177 ( 2004 )

7. Horrocks , I. , Kutz , O. , Sattler , U. : The even more irresistible SROIQ . In: Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning , Lake District of the United Kingdom, June 2-5 , 2006 . pp. 57 { 67 ( 2006 )

8. Hubauer , T. , Legat , C. , Seitz , C. : Empowering adaptive manufacturing with interactive diagnostics: A multi-agent approach . In: Advances on Practical Applications of Agents and Multiagent Systems - 9th International Conference on Practical Applications of Agents and Multiagent Systems, PAAMS 2011 , Salamanca, Spain, 6 - 8 April 2011 . pp. 47 { 56 ( 2011 )

9. Karp , R.M.: Reducibility among combinatorial problems . In: Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22 , 1972 , at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York. pp. 85 { 103 ( 1972 )

10. Klarman , S. , Endriss , U. , Schlobach , S.: ABox abduction in the description logic ALC . Journal of Automated Reasoning 46 ( 1 ), 43 { 80 ( 2011 )

11. Peirce , C.S. : Deduction, induction, and hypothesis . Popular science monthly 13 , 470 { 482 ( 1878 )

12. Petasis , G. , Moller, R., Karkaletsis , V.: BOEMIE: Reasoning-based information extraction . In: Proceedings of the 1st Workshop on Natural Language Processing and Automated Reasoning co-located with 12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2013 ), A Corunna , Spain, September 15th , 2013 . pp. 60 { 75 ( 2013 )

13. Pukancova , J. , Homola , M. : Abductive reasoning with description logics: Use case in medical diagnosis . In: Proceedings of the 28th International Workshop on Description Logics (DL 2015 ), Athens,Greece, June 7-10, 2015 . ( 2015 )

14. Pukancova , J. , Homola , M. : Tableau-based abox abduction for description logics: Preliminary report . In: Proceedings of the 29th International Workshop on Description Logics , Cape Town, South Africa, April 22-25 , 2016 . ( 2016 )

15. Reiter , R.: A theory of diagnosis from rst principles . Artif. Intell . 32 ( 1 ), 57 { 95 ( 1987 )

16. Sirin , E. , Parsia , B. , Grau , B.C. , Kalyanpur , A. , Katz , Y. : Pellet: A practical OWLDL reasoner . Web Semantics: science, services and agents on the World Wide Web 5 ( 2 ), 51 { 53 ( 2007 )

17. Tsarkov , D. , Horrocks , I. , Patel-Schneider , P.F. : Optimizing terminological reasoning for expressive description logics . J. Autom. Reasoning 39 ( 3 ), 277 { 316 ( 2007 )