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 propositional 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 conjunction 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 j= C u H v D). A tableauxbased 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 framework 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 Ch the resulting concept. Then a solution to such an Abduction Problem is a substitution of concept variables with concepts, such that T j= (Ch) v D. Note that in Concept Matching the concept with variables is D, and a solution is a substitution such that T j= C v (D). The remaining of this paper is structured as follows. In the next section, we lay out some definitions and other preliminary 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. 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 2 fh0; h1; h2; : : :g, in place of a concept name. To extend the semantics of SH to concept terms, we let be an assignment : h 7! C 2 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].
set of axioms in ALN , where both C and D are satisfiable in T . A Concept Abduction Problem (CAP), denoted as hC; D; T ; LiC , is finding a concept H 2 ALN such that T 6j= C u H ?, and T j= 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 = 9howPay.CCu9howPay.:https), and W2 for which it is only known that it has some payment method (9howPay.>). Suppose a user has to choose which service best satisfies her demand D = 9howPay.(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 subsumed 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 = 9howPay.(CC u https) = D. Observe that H1;2 is trivially hypothesizing the whole target conclusion, disregarding the fact that the conjunct 9howPay.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 outermost conjunctions. Instead, solutions should take into account the structure of a formula; 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.
concepts in NNF, and let T be a set of axioms in SH. We define abducible concept Ch =: 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 (9R.C) = 9R.(hnew u Rew (C)); Rew (8R.C) = 8R.(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 Ch 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 Ch, its corresponding hypotheses list H = hh0; : : : ; h`i and a list C = hC0; : : : ; C`i of ALE HR+ concepts, we denote with [H=C] the substitution fh0 7! C0; : : : ; h` 7! C`g and with i[H=C], with i = 0; : : : ; `, the substitution of the single variable hi.
be a set of axioms in SH, where both C and D are satisfiable in T and T 6j= CuD v ?. Let H = hh0; : : : ; h`i be the hypotheses list of the abducible concept Ch and A~ = hA0; : : : ; A`i (for Assumptions) be a list of SH concept sets. A Structural Abduction Problem (SAP) for SH, denoted as hC; D; T ; A~iS , is finding a list of concepts H = hH0; : : : ; H`i in ALE HR+ such that
Hi 2 Ai for every i = 0; : : : ; `
T 6j= [H=H](Ch) v ?
T j= [H=H](Ch) v D
(
Following [5] we use PS as a symbol for a SAP, and we denote with SOLSAP (PS ) the set of all solutions to a SAP PS . Observe that we impose the hypotheses in H to be in the DL ALE HR+ , 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 9howPay.(CC u h1) u 9howPay.(:https u h2)
H = hh0; h1; h2i
H = h>; https; >i [H=H](Ch) = > u 9howPay.(CC u https) u 9howPay.(:https u >) Observe that the solution previously computed in Ex.1 is still a solution of the SAP, namely, it is the solution H0 = h9howPay.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, componentwise subsumption, and subsumption in the abducible concept after substitution. Definition 4 (Preference and Maximality). Let PS be a SAP and H0 = hC00; : : : ; C`0i and H00 = hC000; : : : ; C`00i be two solutions in SOLSAP (PS ). We say that: — H0 is structurally-preferred over H00, denoted by H0 vS H00, if for i = 0; : : : ; ` we have T j= Ci00 v Ci0; — H0 is subsumption-preferred over H00, denoted as H0 v H00, if T j= [H=H00](Ch) v [H=H0](Ch); A solution is Structural-maximal if no solution is structurally preferred to it, and Subsumptionmaximal 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.
Proposition 1. Given a SAP PS = hC; D; T ; A~iS and two solutions H0 and H00 in SOLSAP (PS ), 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 always monotonic over v, that is, if C1 v C2 then for every i = 0; : : : ; `, i[hi=C1](Ch) v i[hi=C2](Ch). 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 Ch is fundamental for the maximality criteria. Consider C = :9R.A; without NNF, Ch would be h0 u :9R.(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 Ch 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 Ch). We preferred to use NNF, so that each concept variable h occurs inside 0 negations in Ch, 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 structural preference, while [H=H](Ch) [H=H0](Ch). Hence a different preference criterion is needed.
Definition 5. Given an abducible concept Ch, we introduce the following preorder among variables in H:(i)h0 < hi with i 6= 0; (ii) hi < hp if hp is within a quantification inside the one of hi; (iii) hi < hp if hp is within an existential quantification 9R.(hp u ), hi is within a universal quantification 8R.(hi u ), and both quantifications appear in the same quantification (i.e., they are siblings in the syntactic tree). Now let H0 = hC00; : : : ; C`0i and H00 = hC000; : : : ; C`00i be two solutions in SOLSAP (PS ). 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 = f>; https; >g and H0 = f9howPay.CC u https; >; >g. 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
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 calculus [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 interpretation ( I ; I ) satisfies two tableau labels T(n) and F(n) if: — for every concept C 2 T(n) and every concept D 2 F(n), nI 2 CI and nI 62 DI ; — for every role R 2 T(n; m) and for every role Q 2 F(n; m), (nI ; mI ) 2 RI and (nI ; mI ) 62 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 2 T(n; m) or :R0 2 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 2 F(n; m), it is of the form :R. Hence Q 2 F(n; m) means, in fact, (nI ; mI ) 2 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 proposed 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 ? 2 T(n) or > 2 F(n), for some individual n; 2. either A; :A 2 T(n)
(T-homogeneous) or A; :A 2 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].
We observe that given a TBox T and two concept C and D, it results T j= C v D iff
the tableau starting from C 2 T(
T) if n is an individual such that A 2 T(n) in the branch, and A v C 2 T , then add C to T(n).
F) if n is an individual such that :A 2 F(n) in the branch, and A v C 2 T , then add C to F(n). - rules :
T) if n is an individual such that A 2 T(n) in the branch, and A C 2 T , then add C to T(n).
T) if n is an individual such that :A 2 T(n) in the branch, and A C 2 T , then add C to T(n).
F) if n is an individual such that :A 2 F(n) in the branch, and A C 2 T , then add C to F(n).
F) if n is an individual such that A 2 F(n) in the branch, and A C 2 T , then add :A to F(n).
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 Ch 2 T(
Example 4. Suppose to have the following SAP: C = 9R.(A1 u (A2 t :A3)); D = 9R.(A1 u A2) u 9R.(A3 t :A2); T = ; The tableau computed following rules in Fig. 1 and Fig. 2 is depicted in Fig. 3.
T(
T(
F(
F(
F(
T(
T(
F(
T(
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 B0,
B1 and B2. Once the tableau is closed we know that T j= (Ch) v D. Actually this
relation holds even when trivially T j= (Ch) v ?. Nevertheless, if we want that be
a solution to a SAP, by condition (
Proposition 3. Let T be a TBox, Ch be an abducible concept, H = hh0; : : : ; hli be its cTo(r1r)e;sDpon2diFn(g1h).yFpoortheeasechs loispteannbdranbche aBnj o2pen, cwoimthpjle2te [t0a;b:le: a:u;ks]t,airftinjg[ Hfro=mHjC] his 2a substitution such that j [H=Hj ](Bj ) is closed then [H=H] = fh0 7!
00[H=H0]u: : :u 0k[H=Hk]; : : : ; hl 7! l0[H=H0]u: : :u lk[H=Hk]g is such that T j= [H=H](Ch) v D. We call j [H=Hj ] a branch substitution. Proof.
^ ^ ^ If ij [H=H^j] closes B^j then, by u-rule T) in Fig. 1, B^j is closed also by ij [H=Hj ] u C, being C a generic concept. If C = uj6=^j 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
j ; [ f g := ;; foreach open branch Bj 2 do find a branch substitution j such that Bj is closed with a heterogeneous clash;
:= 1 begin 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 end compute a solution to a General SAP hC; D; T ; A~iS . There a practical problem still Algorithm:abduce Input: SH concepts C, D, acyclic TBox T Output: substitution
:= fH0 7! >; : : : ; Hn 7! >g;
compute a H-Tableau;
if is not closed then
repeat
end
foreacih:=j 2iu dijo;
end
until T 6j= (Ch) v ? ;
end
return ;
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 Bj in a H-Tableau we select all the sets labeled with F(n).
If there is a concept variable hi 2 T(n), we could just pick up a concept C 2 F(n)
and perform the substitution ij = fhi 7! Cg. It is easy to see that ij (Bj ) closes with
at least one heterogeneous clash. (C1) For each branch substitution, in order to close a
3
branch it suffices to have at least one variable whose value is different from > .
Note that, depending on the substitution we choose, we have different solutions for the
same SAP. Suppose we select the substitution 1 = fh0 7! >; h1 7! A3g for B1 in
Fig. 3. It is easy to see that 1 closes both B1 with a heterogeneous clash and B2 with
a homogeneous clash. Hence, in this case we do not need to compute a substitution 2
to close B2. 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
conjunctive substitution hi 7! D1 u D2 closes a branch B then by u-rule T) in Fig. 1
either 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
substitutions for the same variable h0. By Proposition 3 we know that the conjunction
8R.A2 u 8R.(A3 t :A2) u 9R.(A3 t :A2) is a substitution for h0 closing B0, B1
and B2. 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! 8R.(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 2 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] = fh0 7! >; h1 7! A2 u A3g
[H=H0] = fh0 7! 9R.(A1 u A2); h1 7! A3g
(
It is noteworthy that the algorithms we presented in this section compute a sub-optimal 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 Thomogeneous 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.
Algorithm 2: Computation of a branch substitution for information minimal solutions. 1 if hi 2 T(n) and there exists a substitution ij k, with k = 1; : : : ; j such that ij := j k closes Bj then
ij :=i ij k; 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 2 T(n) and hp 2 T(m); choose a concept E 2 F(n) such that E does no contain a conjunction and, if possible, Bj [ fE 2 T(n)g does not close with a T-homogeneous clash;
ij := E; Example 5. Suppose we have to solve the following SAP. C = 8R.(A1 u9S.A2); D = 8T .9S.A3; T = ;; R = fTrans(R); S v R; T v Rg Part of the tableau we compute following rules in Fig. 1 is represented in Fig. 4.
T(
F(
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 = fa1; : : : ; ang (atoms), PA is the problem of finding a subset S A such that T ^S is consistent, and T ^ S j= O. Then, PA can be translated into SAP by (i) letting C = > (hence Ch = > u H0 H0), (ii) expressing T and O as ALC concepts—just replace ^; _ with u; t—and (iii) solving the SAP T j= H0 v O, where T = f> v T g. Since in propositional Logic the Deductive Theorem holds, one could also let C = T , T = ;, and solve the SAP j= 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 syntactic 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 [ f g j= 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. Finally, 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 j= [H=H](Ch) v D, one can always let = [H=H](Ch) as a solution.