A Tableaux-based calculus for Abduction in Expressive Description Logics: Preliminary Results Tommaso Di Noia (1), Eugenio Di Sciascio (1), Francesco M. Donini (2) (1) SisInfLab, Politecnico di Bari, Bari, Italy (2) Università della Tuscia , Viterbo, Italy {t.dinoia,disciascio}@poliba.it,donini@unitus.it 1 Introduction Abduction [12] is a well-known form of common-sense reasoning that has been widely exploited in Artificial Intelligence applications, including formalization of Diagnostic Reasoning [13] and Scene Interpretation [14]. Abduction has been also proposed as a logical tool for formalizing hypothetical reasoning in E-Commerce [7], Negotiation [15] and Web-service Discovery [10], among others. The computation of Propositional Abduction (PA) has been extensively studied, for nearly all criteria that can be adopted for choosing the preferred hypotheses [6]. Also Abductive Logic Programming is well established [9], and its computation resorts on a modification of SLD-resolution. Yet, when the representation language chosen for the application domain is a Description Logic (DL), the picture is far from being complete. Since concepts in a DL are in fact monadic predicates, the definition of Abduction should be extended from a proposi- tional to a first-order setting. A possible definition has been proposed by Di Noia et al. [7]: given concepts C (prior facts), D (target), and a TBox T (background knowledge), a Concept Abduction Problem is finding another concept H such that both (i) the con- junction of C and H—denoted in DL by C u H—is satisfiable in T , and (ii) in all models of T , C u H is subsumed by D (denoted by T |= C u H v D). A tableaux- based calculus for computing Concept Abduction in the DL ALN was devised in [5]. However, although ALN is computationally simple, it is a rather inexpressive DL. We propose here a form of Concept Abduction which is computed extending the frame- work of Concept Matching [2]. In a nutshell, we identify places in the description of C where a hypothesis can be added, and name such places with (all distinct) concept variables H0 , H1 , H2 , . . . We denote C h the resulting concept. Then a solution to such an Abduction Problem is a substitution σ of concept variables with concepts, such that T |= σ(C h ) v D. Note that in Concept Matching the concept with variables is D, and a solution is a substitution σ such that T |= C v σ(D). The remaining of this paper is structured as follows. In the next section, we lay out some definitions and other prelim- inary notions. Then we propose a calculus based on tableaux for finding substitutions, and in Section 4 we propose some strategies for finding “good” substitutions. Finally, we compare our proposal with existing literature. 2 Structural Abduction in SH Here, we admit only unfoldable TBoxes and we denote by v∗ the transitive closure of role inclusion over the RBox R. For the sake of conciseness we assume the RBox as part of the TBox: R ⊆ T . We assume that concepts are always in Negation Normal Form (NNF), where negation in front of a concept is always ”pushed” inside connectives and quantifiers, recursively, till negation is in front of concept names only. In the following, we augment concept expressions by means of concept variables. We call concept term [3] every concept expression formed by using the syntax above, plus the ability of using a concept variable h ∈ {h0 , h1 , h2 , . . .}, in place of a concept name. To extend the semantics of SH to concept terms, we let σ be an assignment σ : h 7→ C ∈ SH that interprets concept variables as concepts in SH, and we define the semantics of h as (σ(h))I . We recall previous definition of Concept Abduction in ALN [7]. Definition 1 (Concept Abduction). Let C, D, be two concepts in ALN , and T be a set of axioms in ALN , where both C and D are satisfiable in T . A Concept Abduction C Problem (CAP), denoted as hC, D, T , Li , is finding a concept H ∈ ALN such that T 6|= C u H ≡ ⊥, and T |= C u H v D. While adequate for Description Logics as ALN , Def. 1 shows its limits when dealing with languages where qualified existential quantification is allowed. This is the case of ALE and, more generally, of ALC and SH. We explain the need to generalize Def. 1 with the aid of a simple example. Example 1. Let W1 , W2 be two Web services, W1 having two payment methods: a Credit-card one and a non-https-based one (W1 = ∃howPay.CCu∃howPay.¬https), and W2 for which it is only known that it has some payment method (∃howPay.>). Suppose a user has to choose which service best satisfies her demand D = ∃howPay.(CCu https). Only for sake of simplicity, let the TBox be empty. Obviously, both W1 6v D and W2 6v D—i.e., neither service completely fulfills D—so the problem arises as to whether there is some logic-based method to compare them. Some researchers [7, 10] propose to automate the choice by solving two (kind of) abduction problems, and compare the results. Namely, they propose to compare some hypotheses H1 and H2 that, when added to W1 and W2 respectively, would make each one of them be sub- sumed by D. Then, an offer with a more generic H should be preferred over one with a more specific H. Following this criterion, an offer W for which H = > is the ”best” choice, since in this case already W v D. Following Def. 1, we would have to find two concepts H1 , H2 such that Wi u Hi v D (i = 1, 2) and in this case it can be verified that both problems admit one subsumption-maximal solution, namely H1 = H2 = ∃howPay.(CC u https) = D. Observe that H1,2 is trivially hypothesiz- ing the whole target conclusion, disregarding the fact that the conjunct ∃howPay.CC in W1 already “covers” part of D. That is, Def. 1 cannot be used to prefer an offer that already partly covers the demand (W1 ) over another (W2 ) that does not1 . 4 The explanation computed in Ex.1 according to Def. 1 involves the whole existential restriction even though only a part of it would be necessary—in this case https. This is because Concept Abduction (and all definitions of PA) only adds hypotheses as out- ermost conjunctions. Instead, solutions should take into account the structure of a for- mula; this amounts to hypothesize pieces of a formula to be added inside the quantifiers of C and not just added as outermost conjunctions. 1 We remark that also the approach in [4] would compute (CC ∧ https) (with  the modality associated with howPay) for both abduction problems. Hence, also their proposal cannot be used to highlight the missing information inside quantifications. Definition 2 (Abducible Concept – Hypotheses List). Let C and D be two SH- concepts in NNF, and let T be a set of axioms in SH. We define abducible concept . C h = h0 u Rew (C), where the rewriting Rew (C) defined recursively as Rew (A) = A; Rew (¬A) = ¬A; Rew (C1 u C2 ) = Rew (C1 ) u Rew (C2 ) Rew (∃R.C) = ∃R.(hnew u Rew (C)); Rew (∀R.C) = ∀R.(hnew u Rew (C)) where by hnew we mean a concept variable not yet appearing in the rewriting2 . We assume that concept variables are numbered progressively, and call hypotheses list of C h the list H = hh0 , h1 , h2 , . . .i. Observe that since C is in NNF, a case for Rew (¬C), with C a generic concept, is not present in the definition of Rew (). Given an abducible concept C h , its corresponding hypotheses list H = hh0 , . . . , h` i and a list C = hC0 , . . . , C` i of ALEHR+ concepts, we denote with σ[H/C] the substitution {h0 7→ C0 , . . . , h` 7→ C` } and with σi [H/C], with i = 0, . . . , `, the substitution of the single variable hi . Definition 3 (Structural Abduction). Let C, D ∈ SH, be two concepts in NNF, and T be a set of axioms in SH, where both C and D are satisfiable in T and T 6|= CuD v ⊥. Let H = hh0 , . . . , h` i be the hypotheses list of the abducible concept C h and à = hA0 , . . . , A` i (for Assumptions) be a list of SH concept sets. A Structural Abduction S Problem (SAP) for SH, denoted as hC, D, T , Ãi , is finding a list of concepts H = hH0 , . . . , H` i in ALEHR+ such that Hi ∈ Ai for every i = 0, . . . , ` (1) T 6|= σ[H/H](C h ) v ⊥ (2) T |= σ[H/H](C h ) v D (3) We call a SAP General when Ai = SH, for every i = 0, . . . , `. Following [5] we use P S as a symbol for a SAP, and we denote with SOLSAP (P S ) the set of all solutions to a SAP P S . Observe that we impose the hypotheses in H to be in the DL ALEHR+ , in which disjunction is not allowed, and negation is allowed only in front of concept names. This restriction is analogous to the one in PA—where the set of abduced hypotheses is always intended as a conjunction—and Abductive Logic Programming—where again the abduced atoms are (implicitly) taken conjunctively. As noted by Marquis [11] for First-order Abduction, if disjunction and full negation are allowed in solutions to an Abduction problem, the most general hypothesis is always ¬C t D, which in fact solves nothing. Hereafter, we always refer to General SAPs. Example 2. Consider W1 and D as in Ex.1. According to Def. 2 and Def. 3 we have W1h = h0 u ∃howPay.(CC u h1 ) u ∃howPay.(¬https u h2 ) H = hh0 , h1 , h2 i H = h>, https, >i σ[H/H](C h ) = > u ∃howPay.(CC u https) u ∃howPay.(¬https u >) Observe that the solution previously computed in Ex.1 is still a solution of the SAP, namely, it is the solution H0 = h∃howPay.CC u https, >, >i. 4 2 A precise procedure to obtain this result would need a global counter, visible by all recursive calls. We skip this technical detail to simplify presentation. Solutions can be compared according to two preference criteria, namely, component- wise subsumption, and subsumption in the abducible concept after substitution. Definition 4 (Preference and Maximality). Let P S be a SAP and H0 = hC00 , . . . , C`0 i and H00 = hC000 , . . . , C`00 i be two solutions in SOLSAP (P S ). We say that: — H0 is structurally-preferred over H00 , denoted by H0 vS H00 , if for i = 0, . . . , ` we have T |= Ci00 v Ci0 ; — H0 is subsumption-preferred over H00 , denoted as H0 v H00 , if T |= σ[H/H00 ](C h ) v σ[H/H0 ](C h ); A solution is Structural-maximal if no solution is structurally preferred to it, and Subsumption- maximal if no solution is subsumption-preferred to it. However, it turns out that subsumption-preference includes structural preference, hence we can safely forget the latter. S Proposition 1. Given a SAP P S = hC, D, T , Ãi and two solutions H0 and H00 in SOLSAP (P S ), if H0 vS H00 then H0 v H00 . Proof. Recall that (Def. 3) both C and D are in NNF. For this form, substitutions are al- ways monotonic over v, that is, if C1 v C2 then for every i = 0, . . . , `, σi [hi /C1 ](C h ) v σi [hi /C2 ](C h ). This is because concept variables appear only in conjunctions, and positively—i.e., inside no negation. Iterating over the list of concept variables, the claim follows. 2 Note that the requirement that C is in NNF before rewriting in C h is fundamental for the maximality criteria. Consider C = ¬∃R.A; without NNF, C h would be h0 u ¬∃R.(A u h1 ), but due to the fact that h1 is added as a conjunction inside an odd number of negations, by substituting h1 with anything different from > we are in fact making C h more generic, not more specific. So, in the criteria for subsumption-maximal solutions, we should now distinguish between h’s occurring inside an even number of negations and h’s occurring inside an odd number of negations (for which the criteria should be reverted: a more generic substitution yields a more specific C h ). We preferred to use NNF, so that each concept variable h occurs inside 0 negations in C h , and use uniform maximality criteria. Recalling Example2, we observe that none of the previous criteria allows us to prefer H to H0 . This is because H and H0 are incomparable under struc- tural preference, while σ[H/H](C h ) ≡ σ[H/H0 ](C h ). Hence a different preference criterion is needed. Definition 5. Given an abducible concept C h , we introduce the following preorder among variables in H:(i)h0 < hi with i 6= 0; (ii) hi < hp if hp is within a quan- tification inside the one of hi ; (iii) hi < hp if hp is within an existential quantification ∃R.(hp u· · ·), hi is within a universal quantification ∀R.(hi u· · ·), and both quantifica- tions appear in the same quantification (i.e., they are siblings in the syntactic tree). Now let H0 = hC00 , . . . , C`0 i and H00 = hC000 , . . . , C`00 i be two solutions in SOLSAP (P S ). We say that H0 ≤ H00 if Ci0 v Ci00 for some i, and for all p such that hi < hp , Cp0 = Cp00 . Example 3. Turning back to Example 2, we remember that H = {>, https, >} and H0 = {∃howPay.CC u https, >, >}. By Definition 5 we see H ≤ H0 . Indeed, we have https v > (C1 v C10 ) for i = 1 and > = > (C2 = C20 ) for i > 1. 4 3 Calculus We present a calculus and algorithms to compute a solution to a SAP as defined in Section 2 for the expressive DL SH. We assume the reader be familiar with tableau cal- culus [16]. Following [5], we will build a prefixed tableau using two labeling functions (to represent true/false prefixed tableaux) T() and F() instead of a single labelling one L(). T() and F() map an individual n to a set of concepts T(n) or F(n) or relate n to another individual m via a role R. More formally, given two individuals n and m in a tableau τ , the formal semantics of T() and F() is as follows. We say that an interpreta- tion (∆I , ·I ) satisfies two tableau labels T(n) and F(n) if: — for every concept C ∈ T(n) and every concept D ∈ F(n), nI ∈ C I and nI 6∈ DI ; — for every role R ∈ T(n, m) and for every role Q ∈ F(n, m), (nI , mI ) ∈ RI and (nI , mI ) 6∈ QI ; — an interpretation satisfies a branch B of τ if it satisfies T(n), F(n), T(n, m) and F(n, m) for every individual n, and for every pair of individuals n, m in B. Given two individual names n and m, m is called an R-successor of n if, for some R0 with R0 v∗ R, m is a successor of n and either R0 ∈ T(n, m) or ¬R0 ∈ F(n, m). Ancestors are definerd as usual. If n is an ancestor of m, we say m is blocked by n if either T(m) ⊆ T(n) or F(m) ⊆ F(n). In order to compute a solution to a SAP, we will build a prefixed tableau τ using the rules in Fig. 1. Since we use two labelling functions, for each classical tableau rule we have we both a T) version and its dual F) version. The only optimization technique we include here is lazy unfolding [1, 8]. We assume concepts are always simplified in NNF and we use C to represent the NNF of a concept C. Given a SH concept in NNF, whenever we have a role Q ∈ F(n, m), it is of the form ¬R. Hence Q ∈ F(n, m) means, in fact, (nI , mI ) ∈ RI too. Unfolding rules for TBox axioms are presented in Fig. 2. We already discussed the need of having C in NNF. For what concerns D, it is just a matter of not doubling the tableaux rules (if D were not in NNF, we would need, e.g., a rule for u and another rule for ¬(... u ....)). In the following we use the definition of homogeneous and heterogeneous clash as pro- posed in [5]. We recall here the definition of homogeneous and heterogeneous clash as proposed in [5]. Definition 6 (Clash). A branch B contains a homogeneous clash if it contains one of the following: 1. either ⊥ ∈ T(n) or > ∈ F(n), for some individual n; 2. either A, ¬A ∈ T(n) (T-homogeneous) or A, ¬A ∈ F(n) (F-homogeneous) for some individual n and some concept name A; B contains a heterogeneous clash if it contains one of the following: 1. T(n) ∩ F(n) contains either A or ¬A for some individual n and some concept name A; We say a branch B is complete iff for each individual name n occurring in A no new rule application is possible both to T(n) and F(n). A complete branch is open if it contains no clash, otherwise it is closed. A complete tableau is open if it contains at least one open branch, otherwise it is closed. Soundness and completeness of the calculus follow from the version without prefixes [8]. u - rules : T) if C u D ∈ T(n), then add both C and D to T(n). F) if C t D ∈ F(n), then add both C and D to F(n). t - rules : T) if C t D ∈ T(n), then add either C or D to T(n). F) if C u D ∈ F(n), then add either C or D to F(n). ∃ - rules : T) if ∃R.C ∈ T(n), n is not blocked, and n has no R-successor m with either C ∈ T(m) or ¬C ∈ F(m), then pick up a new individual m, add R to T(n, m), and let T(m) := {C}. F) if ∀R.C ∈ F(n), n is not blocked, and n has no R-successor m with either C ∈ T(m) or ¬C ∈ F(m), then pick up a new individual m, add ¬R to F(n, m), and let F(m) := {C}. ∀ - rules : T) if ∀R.C ∈ T(n), n is not blocked, and there exists an individual m such that m is an R- successor of n, then add C to T(m). F) if ∃R.C ∈ F(n), n is not blocked, and there exists an individual m such that m is an R- successor of n, then add C to F(m). ∀+ - rules : T) if ∀R.C ∈ T(n), n is not blocked, with Trans(R) ∈ R and: – R v∗ S; – there exists an individual m such that m is an S-successor of n; then add ∀R.C to T(m). F) if ∃R.C ∈ F(n), n is not blocked, with Trans(R) ∈ R and: – R v∗ S; – there exists an individual m such that m is an S-successor of n; then add ∃R.C to F(m). Fig. 1. Expansion Rules 4 Algorithm and Substitution Strategies We observe that given a TBox T and two concept C and D, it results T |= C v D iff the tableau τ starting from C ∈ T(1), D ∈ F(1) is closed. Moreover, we can say that an heterogeneous clash in τ represents in some way an “interaction” between the concepts C and D. An heterogeneous clash can be seen a “clue” that the relation T |= C v D might hold. Whenever a complete tableau τ has one or more open branches B j , if we want the relation T |= C v D hold, then we have to force the closure of all open branches B j in τ . We observe that if we had a tableau τ 0 starting with C ∈ T(1), and τ 0 is closed then T |= C v ⊥, i.e., C is unsatisfiable w.r.t. T . Also notice that in this case, since we have only T() label, all branches will close with a T-homogeneous clash. Proposition 2. Let C, D be two concepts in SH, T be a TBox in SH with T |= C v ⊥. A complete tableaux τ starting with C ∈ T(1) and D ∈ F(1), is such that for each branch B there is at least one T-homogeneous clash. Proof. If T |= C v ⊥, and τ is complete, as a direct consequence, it will surely close all its branches with at least one T-homogeneous clash. 2 v - rules : T) if n is an individual such that A ∈ T(n) in the branch, and A v C ∈ T , then add C to T(n). F) if n is an individual such that ¬A ∈ F(n) in the branch, and A v C ∈ T , then add C to F(n). ≡ - rules : T) if n is an individual such that A ∈ T(n) in the branch, and A ≡ C ∈ T , then add C to T(n). T) if n is an individual such that ¬A ∈ T(n) in the branch, and A ≡ C ∈ T , then add C to T(n). F) if n is an individual such that ¬A ∈ F(n) in the branch, and A ≡ C ∈ T , then add C to F(n). F) if n is an individual such that A ∈ F(n) in the branch, and A ≡ C ∈ T , then add ¬A to F(n). Fig. 2. Unfolding Rules Note that in this case, in order to catch the inconsistency of C, we need τ to be complete. Given two concepts C, D and a TBox T in SH, we call H-Tableau a complete tableau built starting from C h ∈ T(1) and D ∈ F(1). Example 4. Suppose to have the following SAP: C = ∃R.(A1 u (A2 t ¬A3 )); D = ∃R.(A1 u A2 ) u ∃R.(A3 t ¬A2 ); T = ∅ The tableau computed following rules in Fig. 1 and Fig. 2 is depicted in Fig. 3. T(1) = {h0 u ∃R.(A1 u (A2 t ¬A3 ) u h1 )} F(1) = {∃R.(A1 u A2 ) u ∃R.(A3 t ¬A2 )} T(1) = {h0 , ∃R.(A1 u (A2 t ¬A3 ) u h1 )} T(1, 2) = {R} T(2) = {A1 , A2 t ¬A3 , h1 } F(1) = {∃R.(A1 u A2 )} F(1) = {∃R.(A3 t ¬A2 )} F(2) = A1 u A2 F(2) = {A3 , ¬A2 , A3 t ¬A2 } T(2) = {A2 } T(2) = {¬A3 } open branch B1 open branch B2 F(2) = {A1 } F(2) = {A2 } × heterogeneous clash A1 ∈ F(2) and A1 ∈ T(2) T(2) = {A2 } T(2) = {¬A3 } × open branch B0 heterogeneous clash A2 ∈ F(2) and A2 ∈ T(2) Fig. 3. A H-Tableau computed applying expansion rules in Fig. 1 and Fig. 2. Looking at Fig. 3 we observe that we could close the tableau by substituting the two concept variables h0 and h1 with concepts generating a clash in the open branches B 0 , B 1 and B 2 . Once the tableau is closed we know that T |= σ(C h ) v D. Actually this relation holds even when trivially T |= σ(C h ) v ⊥. Nevertheless, if we want that σ be a solution to a SAP, by condition (2) of Def. 3, we have to avoid that. By Proposition 2, we know that in order to have T 6|= σ(C h ) v ⊥, it suffices to have at least one branch closed by a heterogeneous clash. Hence, in order to compute σ we will look for instantiation of variable in the hypotheses list H of C h such that, given a complete open tableau τ , there is at least one open branch B ∈ τ such that σ(B) closes without any homogeneous clash. Proposition 3. Let T be a TBox, C h be an abducible concept, H = hh0 , . . . , hl i be its corresponding hypotheses list and τ be an open complete tableau starting from C h ∈ T(1), D ∈ F(1). For each open branch B j ∈ τ , with j ∈ [0, . . . , k], if σ j [H/Hj ] is a substitution such that σ j [H/Hj ](B j ) is closed then σ[H/H] = {h0 7→ σ00 [H/H0 ]u. . .uσ0k [H/Hk ], . . . , hl 7→ σl0 [H/H0 ]u. . .uσlk [H/Hk ]} is such that T |= σ[H/H](C h ) v D. We call σ j [H/Hj ] a branch substitution. Proof. If σiĵ [H/Hĵ ] closes B ĵ then, by u-rule T) in Fig. 1, B ĵ is closed also by σiĵ [H/Hĵ ] u C, being C a generic concept. If C = uj6=ĵ σij [H/Hj ] the proposition holds. 2 For the sake of clarity, when no confusion arises, from now on we will write σ to denote σ[H/H], σi to denote σi [H/H], σ j to denote σ j [H/Hj ] and σij to denote σij [H/Hj ]. Algorithm 1 shows how to compute a solution to SAPs using prefixed tableaux. Some Desiderata for σ[H/H]: In Algorithm 1 we propose a greedy procedure to Algorithm 1: An Algorithm to compute a solution to a SAP Algorithm:abduce Input: SH concepts C, D, acyclic TBox T Output: substitution σ 1 begin 2 σ := {H0 7→ >, . . . , Hn 7→ >}; 3 compute a H-Tableau; 4 if τ is not closed then 5 repeat 6 Θ := ∅; 7 foreach open branch Bj ∈ τ do 8 find a branch substitution σ j such that Bj is closed with a heterogeneous clash; 9 Θ := Θ ∪ {σ j }; 10 end 11 foreach σ j ∈ Θ do 12 σi := σi u σij ; 13 end 14 until T 6|= σ(C h ) v ⊥ ; 15 end 16 return σ; 17 end S compute a solution to a General SAP hC, D, T , Ãi . There a practical problem still remains: the computation of the branch substitution σ j in line 8. There are different strategies to compute σ j depending on the characteristics we desire to be shown by σ. In this section we identify and discuss some properties of σ that can be easily computed (implemented) given a H-Tableau, lead by information minimal criteria. In other words, we would like to have a practical (from an implementation point of view) procedure able to compute a solution to a SAP that shows some information minimal properties. The first practical issue we face is: given a H-Tableau, in case we want to solve a General SAP, how could we select concepts in SH in order to close open branches? We could perform a syntactic search of such concepts looking at the H-Tableau itself: (C0) For each open branch B j in a H-Tableau we select all the sets labeled with F(n). If there is a concept variable hi ∈ T(n), we could just pick up a concept C ∈ F(n) and perform the substitution σij = {hi 7→ C}. It is easy to see that σij (B j ) closes with at least one heterogeneous clash. (C1) For each branch substitution, in order to close a branch it suffices to have at least one variable whose value is different from >3 . Note that, depending on the substitution we choose, we have different solutions for the same SAP. Suppose we select the substitution σ 1 = {h0 7→ >, h1 7→ A3 } for B 1 in Fig. 3. It is easy to see that σ 1 closes both B 1 with a heterogeneous clash and B 2 with a homogeneous clash. Hence, in this case we do not need to compute a substitution σ 2 to close B 2 . Since we are looking for information minimal hypotheses, in case we are willing to compute, for each variable, conjunction minimal substitutions: (C2) we should avoid variable substitution in conjunctive form. In fact, if a conjunc- tive substitution hi 7→ D1 u D2 closes a branch B then by u-rule T) in Fig. 1 ei- ther hi 7→ D1 or hi 7→ D2 closes B; (C3) when computing a branch substitution for an open branch, we have to take into account also the substitutions of the other open branches. With respect to Example 4 we see that there are three different sub- stitutions for the same variable h0 . By Proposition 3 we know that the conjunction ∀R.A2 u ∀R.(A3 t ¬A2 ) u ∃R.(A3 t ¬A2 ) is a substitution for h0 closing B 0 , B 1 and B 2 . Hence, if a variable substitution closes more than one open branch, i.e., the same variable substitution appears in more than one branch substitution, it should be preferred over the others. This is the case, for instance, of h0 7→ ∀R.(A3 t ¬A2 ) for σ 1 and σ 2 ; Going back to Condition (C0) and Condition (C1), given a H-Tableau, in case there is more than one individual n such that hi ∈ T(n), how to choose the individual? What is the best candidate? Moreover, once we choose and individual n, which concept in F(n) should we pick-up? It depends on the solution we want to compute. (C4) With respect to Example 4, if we consider either σ 0 in row 3 or σ 0 in row 4 and σ 1 in row 11 we obtain4 : σ[H/H00 ] = {h0 7→ >, h1 7→ A2 u A3 } (4) σ[H/H0 ] = {h0 7→ ∃R.(A1 u A2 ), h1 7→ A3 } (5) Note that both H0 and H00 are computed satisfying all the above conjunction minimal conditions. Nevertheless, we see that solutions (4) is more “fine-grained” than solu- 3 Branch substitutions with all the variables in H but one equal to > tend to generate structural maximal solutions. 4 In this case it suffices to have h1 7→ A3 in σ 1 to close both B1 and B2 . tion (5). Also notice that σ[H/H0 ](C h ) v σ[H/H00 ](C h ). In other words, solutions (4) is subsumption-maximal w.r.t. solution (5). With respect to Definition 5 it results H0 ≤ H00 . Hence, when closing an open branch B to compute a subsumption maximal solution we tend to select variable hi ∈ T(n) such that there is no hp ∈ T(m) with hi < hp . In Algorithm 2 we propose a procedure to compute a branch substitution σ j taking into account (C0), (C1), (C2), (C3) and (C4). Moreover, from Proposition 2 we know that if there is at least one branch B j in a H-Tableau such that B j does not contain any T-homogeneous clash, then T 6|= σ(C h ) v ⊥. In order to catch this situation as soon as possible, while computing σ j we should avoid, if possible, to close B j generat- ing also a T-homogeneous clash.5 — In line 1 of Algorithm 2 we take into account Condition (C3). Indeed, given B j we try to reuse a substitutions already computed for previous branches B j−k . — Line 4 formalizes conditions (C0) and (C4). We select an individual n such that both T(n) contains hi and there is no other h-variable hp such that it is “bigger” than hi . — Since we selected n such that F(n) 6= ∅, we can choose a concept in F(n) to close B j . Furthermore, while closing B j we try to avoid heterogeneous clashes in order to discard inconsistent substitutions (see Proposition 2). It is noteworthy that the algorithms we presented in this section compute a sub-optimal Algorithm 2: Computation of a branch substitution for information minimal so- lutions. 1 if hi ∈ T(n) and there exists a substitution σij−k , with k = 1, . . . , j such that σij := σij−k closes Bj then 2 σij := σij−k ; 3 else 4 select an individual n such that T(n) 6= ∅,F(n) 6= ∅ and there exists no other individual m such that both T(m) 6= ∅, F(m) 6= ∅ and hi < hp with hi ∈ T(n) and hp ∈ T(m); 5 choose a concept E ∈ F(n) such that E does no contain a conjunction and, if possible, Bj ∪ {E ∈ T(n)} does not close with a T-homogeneous clash; 6 σij := E; 7 end 8 foreach hk ∈ H with k 6= i do 9 σkj := >; 10 end solution due to their greedy nature. In fact, we have no guarantee that Algorithm 2 finds a substitution such that σ[H/H](τ ) have at least one branch closed by no T- homogeneous clash. However, the algorithms we illustrated in this section are very useful to understand the issues related to the computation of a solution to a SAP. Dealing with RBoxes: It is easy to see that Algorithm 2 works nicely when R = ∅. Let us take a look at what happens when we have to deal with a non-empty RBox. 5 We minimize T-homogeneous clashes in order to avoid trivial solutions. Example 5. Suppose we have to solve the following SAP. C = ∀R.(A1 u∃S.A2 ); D = ∀T .∃S.A3 ; T = ∅; R = {Trans(R), S v R, T v R} Part of the tableau we compute following rules in Fig. 1 is represented in Fig. 4. T(1) = {h0 u ∀R.(h1 u A1 u ∃S.(h2 u A2 ))} F(1) = {∀T .∃S.A3 } T(1) = {h0 , ∀R.(h1 u A1 u ∃S.(h2 u A2 ))} F(1, 2) = {¬T } F(2) = {∃S.A3 } T(2) = {h1 , A1 , ∃S.(h2 u A2 ), ∀R.(h1 u A1 u ∃S.(h2 u A2 ))} T(2, 3) = {S} T(3) = h2 , A2 , h1 , A1 , ∃S.(h2 u A2 ), ∀R.(h1 u A1 u ∃S.(h2 u A2 )) F(3) = A3 ... ... Fig. 4. Part of the tableau computed for Example 5 Looking at Example 5 we see that, due to R, both h1 and h2 appears in T(3). Hence, following Algorithm 2 we can close the branch with one of the following two substi- tutions: σ[H/H0 ] = {h0 7→ >, h1 7→ >, h2 7→ A3 }; σ[H/H00 ] = {h0 7→ >, h1 7→ A3 , h2 7→ >} Due to Trans(R), we have σ[H/H00 ](C h ) v σ[H/H0 ](C h ). Similarly to what we do in (C4), if we are looking for subsumption-maximal solutions we will prefer H0 over H00 3. On the other hand we see that H0 ≤ H00 . Hence, (C4) holds also in presence of a non-empty RBox. 5 Remarks and Conclusion We claim that our proposal is a proper extension of PA. In fact, given a theory T , some observations O (both propositional formulas) and a set of possible assumptions A = {a1 , . . . , an } (atoms), PA is the problem of finding a subset S ⊆ A such that T ∧S is consistent, and T ∧S |= O. Then, PA can be translated into SAP by (i) letting C = > (hence C h = > u H0 ≡ H0 ), (ii) expressing T and O as ALC concepts—just replace ∧, ∨ with u, t—and (iii) solving the SAP T |= H0 v O, where T = {> v T }. Since in propositional Logic the Deductive Theorem holds, one could also let C = T , T = ∅, and solve the SAP |= T u H0 v O. In both cases only substitutions involving atoms in A should be considered. Hence, SAP properly extends PA. Given that ALC is a syn- tactic variant of the Modal Logic Kn , and that (the Modal Logic version of) transitive roles is present in the Modal Logic S4, the work most similar to ours is [4]. Compared to our work, Cialdea & Pirri did not have our known facts C. Moreover, they looked for formulas α such that T ∪ {α} |= O, that in our setting could be rephrased as CA of Section 2, or alternatively, as a SAP having on H0 as variable to be substituted. Fi- nally, they just looked for subsumption-maximal abductions on H0 , while our approach allows us to find several abduction solutions depending on the preference criterion for the various Hi ’s. On the other hand, every solution we find can be turned into a solution in their framework: in fact, given a solution σ[H/H], since T |= σ[H/H](C h ) v D, one can always let α = σ[H/H](C h ) as a solution. References 1. F. Baader, B. Hollunder, B. Nebel, H. Profitlich, and E. Franconi. An empirical analysis of optimization techniques for terminological representation systems or “making KRIS get a move on”. In proc. of KR’92, 1992. 2. F. Baader, R. Küsters, A. Borgida, and D. L. McGuinness. Matching in description logics. Journal of Logic and Computation, 9(3), 1999. 3. F. Baader and P. Narendran. Unification of concept terms in description logics. Journal of Symbolic Computation, 31(3), 2001. 4. M. Cialdea Mayer and F. Pirri. Modal propositional abduction. Journal of the IGPL, 3(6), 1995. 5. S. Colucci, T. Di Noia, E. Di Sciascio, F. Donini, and M. Mongiello. A Uniform Tableaux- Based Method for Concept Abduction and Contraction in Description Logics. In proc. of ECAI’04, 2004. 6. N. Creignou and B. Zanuttini. A complete classification of the complexity of propositional abduction. SIAM J. Comput., 36(1), 2006. 7. T. Di Noia, E. Di Sciascio, and F. M. Donini. Semantic matchmaking as non-monotonic reasoning: A description logic approach. Journal of Artificial Intelligence Research, 29:269– 307, 2007. 8. I. Horrocks. Using an expressive description logic: FaCT or fiction? In proc. of KR ’98, 1998. 9. A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive logic programming. Journal of Logic and Computation, 2(6), 1992. 10. F. Lécué, A. Delteil, and A. Léger. Applying abduction in semantic web service composition. In proc. of ICWS’07. 11. P. Marquis. Extending abduction from propositional to first-order logic. In proc. of FAIR’91, 1991. 12. C. Peirce. Abduction and induction. In Philosophical Writings of Peirce. J. Buchler, 1955. 13. H. E. Pople. On the mechanization of abductive logic. In proc of IJCAI’73, 1973. 14. R. Reiter and A. K. Mackworth. A logical framework for depiction and image interpretation. Artificial Intelligence, 41, 1989. 15. C. Sakama and K. Inoue. Negotiation by abduction and relaxation. In proc. of AAMAS’07, 2007. 16. R. M. Smullyan. First-Order Logic. Springer-Verlag, 1968.