Abductive reasoning through δ-resolution

Abductive Reasoning Through δ-Resolution Fernando Soler-Toscano∗ Abstract: In order to explore the duality between deductive and abductive reasoning, we present a propositional calculus, named δ-resolution, dual to the resolution one. We say it is an abductive calculus because every formula we obtain is not a logical consequence of the premises, but an hypothesis of them. Within this calculus we define an abductive process which produces, for a given abductive problem, every minimal abductive hypothesis. Keywords: MSC code: 1 Introduction Abduction is a way of reasoning which goes in search of a plausible explanation αfor a given fact φ, within a background theory Θ. When an abductive problem arises, Θ 2φ; then αis an abductive solution if (among other requisites that will be introduced later) Θ, α φ. Many logical and computational approaches have been proposed to formalize the abductive reasoning. But most of them [1, 3] lie in abductive uses of abductive calculi. That is, those approaches do not define an abductive calculus, but they establish techniques to use existing deductive calculi in an abductive way, so the products (formulas) they obtain are correct abductive solutions. In this paper we present the δ-resolution calculus, dual to standard resolution. Within this calculus, given a set of formulas A(we call this set a δ-clausal form), we obtain formulas Σ (δ-clauses) such that Σ A, so the obtained formulas entail the original set, not the reverse (as in standard deductive calculi). For this reason, we consider δ-resolution a proper abductive calculus. In section 2 we introduce the ∗This paper was written in the context of the research project HUM2004-01255, from the Spanish Ministry of Education and Science. Also, the author is supported by a grant for early stage researchers from the Andalusian Department of Innovation, Science and Business. 347 348 Fernando Soler-Toscano basic definitions of abductive problem and abductive solution. In section 3 the δ-resolution calculus and its main properties are presented. Then, section 4 defines an abductive process by using only the δ-resolution calculus, which produces all the minimal abductive solutions for a given abductive problem. 2 Preliminaries We center our analysis in classical propositional logic. We take Lpas a propositional language, defined with the habitual connectives ∨,∧,→and ¬. We use lower-case Greek letters for formulas and upper-case Greek letters for sets of formulas. If λis a literal (positive or negative), λrepresents its complementary (negative or positive, respectively). The logical consequence relation, , is taken as usual. Definition 1 (Abductive problem) Given Θ⊂ Lpand φ∈ Lp,hΘ, φiis an abductive problem iff Θ2φ(1) Θ2¬φ(2) Definition 2 (Abductive solution) The set of literals Σ⊂ Lpis an abductive solution for the abductive problem hΘ, φiiff Θ∪Σφ(3) Θ∪Σ2⊥(4) Σ2φ(5) For every Σ0⊂Σ,Θ∪Σ02φ(6) We represent as Abd(Θ, φ)the set of abductive solutions for the abductive problem hΘ, φi. Definition 3 (Minimal model) A satisfiable set of literals Σ⊂ Lpis a minimal model of α∈ Lpiff Σα(7) For every Σ0⊂Σ,Σ02α(8) Observation 4 A direct conclusion from definition 3 is that for every satisfiable set of literals Σ⊂ Lpand every formula α∈ Lp, if Σα, then there is aΣ0⊆Σwhich is a minimal model of α. Observation 5 From definition 3, and using the deduction theorem, we can transform the requisites (3) and (6) of definition 2 (provided that, by (4),Σ must be satisfiable) in Σis a minimal model of ¬θ∨φ(9) Abductive Reasoning Through δ-Resolution 349 where θis Vη∈Θη, since Θ∪Σφ,Σθ→φ, and Σ¬θ∨φare equivalent. Also, requisites (4) and (5) of definition 2 can be transformed, respectively, in Σ2¬θ(10) Σ2φ(11) Then, Σis an abductive solution for the abductive problem hΘ, φiiff (9)–(11). 3 The δ-resolution calculus Definition 6 (δ-clause) Aδ-clause Σ = {λ1, . . . , λn}is a finite set of literals of Lp. Given a boolean valuation v,vΣiff vλi, for every λi, 1≤i≤n. With ♦we represent the empty δ-clause, which is universally valid. Definition 7 (δ-clausal form) Aδ-clausal form A={Σ1, . . . , Σn}is a finite set of δ-clauses. Given a boolean valuation v,vAiff vΣifor at least one of the Σi,1≤i≤n. The empty δ-clausal form is not satisfiable. Given α∈ Lp, if Ais equivalent to α, we say it is the δ-clausal form of α. Observation 8 For a given formula α∈ Lpthere are many δ-clausal forms equivalent to it. But we can refer to Aas the δ-clausal form of αbecause for every other δ-clausal form Bequivalent to α, it is obvious that A↔B. Theorem 9 (Conversion to δ-clausal form) For each α∈ Lp, there is a δ-clausal form Asuch that αand Aare equivalent. Proof: Let (λ1 1∧. . . ∧λj1 1)∨. . . ∨(λ1 n∧. . . ∧λjn n) be the disjunctive normal form of α. Then, A={{λ1 1, . . . , λj1 1}, . . . , {λ1 n, . . . , λjn n}} is equivalent to α.  Observation 10 Given the δ-clausal form A={Σ1, . . . , Σn}, if each Σi= {λ1 i, . . . , λji i}, for any Σi,1≤i≤n, then every formula α∈ Lpequivalent to (λ1 1∧. . . ∧λj1 1)∨. . . ∨(λ1 n∧. . . ∧λjn n)has Aas its δ-clausal form. In this way, we can obtain, for each δ-clausal form A, a formula αsuch that Ais its δ-clausal form. Definition 11 (δ-resolution rule) Given two δ-clauses Σ1∪ {λ}and Σ2∪ {¬λ}, the δ-resolution rule produces their δ-resolvent Σ1∪Σ2: Σ1∪ {λ}Σ2∪ {¬λ} Σ1∪Σ2 350 Fernando Soler-Toscano Though this rule is presented with the same format than the standard resolution rule, they are different since now we are working with δ-clauses. In the standard resolution calculus [6], every obtained clause is a logical consequence of the original set. Now, as we prove in theorem 13, any δ-clausal form which contains Σ1∪ {λ}and Σ2∪ {¬λ}is a logical consequence of Σ1∪Σ2. Definition 12 (Proof by δ-resolution) The δ-clause Σis provable by δresolution from the δ-clausal form A, what we express with A`δΣ, iff there is a sequence of δ-clauses such that: •Each δ-clause of the sequence is either a member of Aor a δ-resolvent of previous δ-clauses. •The last δ-clause of the sequence is Σ. Theorem 13 (Soundness) For every δ-clausal form Aand δ-clause Σ, if A`δΣ, then ΣA. Proof: The proof is made by an induction on the number of applications of the δ-resolution rule. In the base case (0 applications), Σ ∈A, and by definition 7, Σ A. For the induction step, let us consider that until the nth application, every resulting δ-clause entails A. Then, let Σ = Σ1∪Σ2be the n+1th δ-clause obtained, a δ-resolvent of Σ1∪{λ}and Σ2∪{¬λ}. Then, every boolean valuation vwhich satisfies Σ satisfies one of the previous δ-clauses, because vshould satisfy every literal of Σ1∪Σ2and vλor v¬λ. Finally, by using the induction hypothesis, vsatisfies A. So, Σ A. Theorem 14 (Completeness) If Ais an universally valid δ-clausal form, then A`δ♦. Proof: Let sbe the cardinality of Aand tthe sum of the cardinalities of all the δ-clauses of A. Take k=t−s. We proceed by induction on the value of k, by considering that ♦/∈A(to avoid the trivial case, where it is obvious that A`δ♦). When k= 0, the only possibility is that Ais a set of unary δ-clauses. Then, if Ais universally valid, it should contain two δ-clauses {λ} and {¬λ}. Whit only one application of the δ-resolution rule, we get ♦. Suppose that the theorem is valid for k≤n, we will prove it for k=n+1. In this case, there is in Aone δ-clause Σ = {λ1, λ2, . . . , λm}, where m≥2. Then, we define Σ0={λ1}, and Σ00 ={λ2, . . . , λm}. But, if Ais universally valid, then (A−Σ) ∪ {Σ0}and (A−Σ) ∪ {Σ00}are also universally valid (it is a direct conclusion from definitions 6 and 7), and for these sets, k≤n, so we can get ♦from them, through the proofs (sequences of δ-clauses) Dem0and Dem00, respectively. Let Dem be a proof from A, constructed in a similar way that Dem00, but each time Σ00 is used in Dem00, Σ is used in Dem. Then, as Abductive Reasoning Through δ-Resolution 351 the only difference between Σ00 and Σ is that Σ contains λ1, the last δ-clause in Dem is either ♦(in that case A`δ♦, and the proof finishes) or {λ1}. In the last case, we have on the proof all the δ-clauses of (A−Σ) ∪ {Σ0}(as Σ0 is {λ1}), and we can complete it as Dem0to get ♦. Theorem 15 (Abductive Completeness) Let Abe the δ-clausal form of α∈ Lp. Then, A`δΣfor each Σwhich is a minimal model of α. Proof: If Σ = {λ1, . . . , λn}is a minimal model of α, then, by definition 3, Σα, so applying the deduction theorem, (λ1∧. . . ∧λn)→α, and by evaluation of →and ¬,λ1∨. . . ∨λn∨α. As A∪ {{λ1}, . . . , {λn}} is the δ-clausal form of the latter formula, we have that, for being universally valid, it is possible to get ♦from it (theorem 14), through a proof we call Dem. In a similar way that we did when proving the completeness theorem, we construct a proof parallel to Dem, called Dem0, which only uses δ-clauses of A. Now, when a δ-clause of type {λi}, 1 ≤i≤n, is used in Dem, nothing is done in Dem0. It is easy to observe that the last δ-clause of Dem0should be a Σ0⊆Σ, because, each δ-clause {λi}can only eliminate the literal λiin the proof. But if Σ0⊂Σ, as by theorem 13, Σ0A, then Σ0α, what is contrary to the supposition that Σ is a minimal model of α. So, Σ0= Σ.  Definition 16 (Subsumption) We say that the δ-clause Σ0subsumes the δ-clause Σiff Σ0⊂Σ. Corollary 17 (Subsumption rule) For δ-clauses Γ,Σand Λ, and each δclausal form A, if A∪ {Σ} ∪ {Σ∪Λ} `δΓand Γis satisfiable, then there is aδ-clause Γ0such that A∪ {Σ} `δΓ0and Γ0⊆Γ. Proof: If we eliminate Σ ∪Λ from A∪ {Σ} ∪ {Σ∪Λ}, the resulting δ-clausal form, A∪ {Σ}, is equivalent to the former, as one can easily observe by a simple semantical reasoning, based on definitions 6 and 7. For theorem 13, ΓA∪ {Σ}∪{Σ∪Λ}, and using the above mentioned equivalence, Γ  A∪ {Σ}. But, let α∈ Lpbe a formula with A∪ {Σ}as its δ-clausal form (observation 10). Then, Γ αand, by observation 4, there is a Γ0⊆Γ such that Γ0is a minimal model of α. Then, for theorem 15, A∪ {Σ} `δΓ0. Corollary 18 (Elimination of contradictory δ-clauses) For each satisfiable δ-clause Σ, each δ-clausal form Aand each literals λ,¬λ,γ1, ...,γn, if A∪ {{λ, ¬λ, γ1, . . . , γn}} `δΣ, then there is a Σ0⊆Σsuch that A`δΣ0. Proof: As {λ, ¬λ, γ1, . . . , γn}is not satisfiable, A∪ {{λ, ¬λ, γ1, . . . , γn}} is equivalent to A(definitions 6 and 7). So, for theorem 13, Σ A. Let α 352 Fernando Soler-Toscano be a formula with Aas its δ-clausal form (observation 10). Then, Σ α and, following the observation 4, Σ0⊆Σ is a minimal model of α. So, by theorem 15, A`δΣ0. Definition 19 (Saturation) Given the δ-clausal form A, the set saturation by δ-resolution from A, that we represent as Aδ, is the minimal set which contains every δ-clause Σsuch that •Σis satisfiable. •A`δΣ. •There is not Σ0⊂Σsuch that A`δΣ0. Observation 20 Given a finite set of δ-clauses A,Aδis also finite. The reason is that the set of possible δ-clauses formed from a finite set of literals U(the literals which appear in A) is exactly P(U)(the power set of U). Then, Aδis a subset of the former and it should be completed in a finite number of applications of the δ-resolution rule, when it is not possible to generate any new δ-clause. Corollary 21 (Fundamental property of saturation) Let Abe the δ-clau- sal form of α. Then, Aδis the set of minimal models of α. Proof: Theorem 15 states that every Σ which is a minimal model of αis provable by δ-resolution from A. So, by definition 19, Σ should belong to Aδ, because Σ is satisfiable (definition 3) and there is no Σ0⊂Σ such that A`δΣ0(because then, by theorem 13, Σ0A, and it contradict that Σ is a minimal model of α). So, every minimal model of αbelongs to Aδ. On the other hand, let us prove that every δ-clause Σ of Aδis a minimal model of α. As, by definition 19, Σ is satisfiable and A`δΣ, so Σ A(theorem 13) and Σ α(definition 7), the only way of not being Σ a minimal model of αis (observation 4) that Σ0⊂Σ is a minimal model of α. But then, by theorem 15, A`δΣ0, what contradicts what definition 19 states about Σ. So, Σ is a minimal model of α. Observation 22 Given A, a way for constructing Aδis to obtain every possible δ-resolvent from the original δ-clauses and those which appear, and then eliminate all the contradictory and subsumed ones. But this process may be hard (anyway, its complexity is exponential), so it will be good to use (specially in an implementation) some kind of searching strategies, like those followed by resolution theorem provers. As, thought semantically dual, δ-resolution calculus is syntactically identical to de classical resolution one, it is possible to use in the former the same searching strategies of the latter. For example, Abductive Reasoning Through δ-Resolution 353 corollaries 17 and 18 allow us to eliminate the subsumed and contradictory δ-clauses in any moment, without waiting until the end of the process. Theorem 23 (Fundamental theorem of δ-resolution) For a given abductive problem h{θ1, . . . , θn}, φi, if NΘand Oare respectively the δ-clausal forms of ¬(θ1∧. . . ∧θn)and φ, then Abd (Θ, φ) = Nδ Θ∪Oδδ−Nδ Θ∪Oδ Proof: First, consider that Σ ∈ Abd(Θ, φ). As explained in observation 5, this means that: •Σ is a minimal model of ¬(θ1∧. . . ∧θn)∨φ. But this formula has NΘ∪Oas its δ-clausal form, so by corollary 21, Σ ∈(NΘ∪O)δ. But (Nδ Θ∪Oδ)δ= (NΘ∪O)δ(the order in which the δ-resolution rule is applied to the δ-clauses of a set Adoes not change the resulting set Aδ), so Σ ∈(Nδ Θ∪Oδ)δ. •Σ2¬(θ1∧. . . ∧θn), and Σ 2φ. So, by definition 3, Σ is not a minimal model of ¬(θ1∧. . . ∧θn) nor of φ, so by corollary 21, Σ /∈Nδ Θand Σ/∈Oδ, respectively. Hence, Σ ∈(Nδ Θ∪Oδ)δ−(Nδ Θ∪Oδ). Now, suppose that Σ ∈(Nδ Θ∪Oδ)δ− (Nδ Θ∪Oδ) to prove Σ ∈ Abd(Θ, φ). We have: •Σ∈(Nδ Θ∪Oδ)δ. As observed above, this is equivalent to Σ ∈(NΘ∪O)δ, and for being NΘ∪Othe δ-clausal form of ¬(θ1∧. . . ∧θn)∨φ, then by corollary 21, Σ is a minimal model of ¬(θ1∧. . . ∧θn)∨φ. •Σ/∈Nδ Θ. Then, given that NΘis the δ-clausal form of ¬(θ1∧. . .∧θn), by corollary 21 we have that Σ is not a minimal model of ¬(θ1∧. . . ∧θn). But suppose that Σ ¬(θ1∧. . . ∧θn); then, by observation 4, there is a Σ0⊂Σ such that Σ0is a minimal model of ¬(θ1∧. . . ∧θn). But then Σ0∈Nδ Θ(corollary 21), and this contradict that Σ ∈(Nδ Θ∪Oδ)δ, because Σ is subsumed by Σ0. So, Σ 2¬(θ1∧. . . ∧θn). •Σ/∈Oδ. Then, as Ois the δ-clausal form of φ, by corollary 21 we have that Σ is not a minimal model of φ. Suppose that Σ φ. Then, by observation 4, there is a Σ0⊂Σ such that Σ0is a minimal model of φ, and so Σ0∈Oδ(corollary 21), and this contradict that Σ ∈(Nδ Θ∪Oδ)δ, because Σ is subsumed by Σ0. So, Σ 2φ. Hence, by observation 5, Σ ∈ Abd(Θ, φ).  Corollary 24 Given α, β ∈ Lpsuch that their δ-clausal forms are, respectively, Aand B, then αβiff for every Σ∈Aδthere is a Σ0⊆Σsuch that Σ0∈Bδ. 354 Fernando Soler-Toscano Proof: Suppose that αβand Σ ∈Aδ. Then, by corollary 21, Σ is a minimal model of α, and by definition 3 this means that Σ α. But αβ, so Σ β. As commented in observation 4, there is a Σ0⊆Σ such that Σ0is a minimal model of β. So, by corollary 21, Σ0∈Bδ. Now suppose that for every Σ ∈Aδthere is a Σ0⊆Σ such that Σ0∈Bδ, in order to prove that αβ. Let vbe any boolean valuation such that vα. Then, let Σ?be the δ-clause composed by all the literals satisfied by v which are either propositional variables occurring in αor their negations. It is obvious that Σ?α. Then (observation 4) there exists a δ-clause Σ ⊆Σ? such that Σ is a minimal model of α, and by corollary 21, Σ ∈Aδ. Then, there is a Σ0⊆Σ such that Σ0∈Bδ. So, Σ0is a minimal model of β, and so Σ0β, and as Σ0⊆Σ?,vΣ0and then vβ. So, αβ. 4 An abductive process by δ-resolution Theorem 23 establishes that for a given abductive problem hΘ, φiit is possible to find the set Abd(Θ, φ) by only δ-resolution operations. In this section we present an sketch of an abductive process that, for a given pair hΘ, φifirst determines whether it is an abductive problem (by studying semantically Θ, φand their relation) and only in the positive case constructs Abd(Θ, φ). This is all done by δ-resolution. Algorithm 25 (Abductive process) The input is hΘ, φi,Θ = {θ1, . . . , θn}, where Θ⊂ Lpand φ∈ Lp. Then: Step 1: Theory Analysis. Let NΘbe the δ-clausal form of ¬(θ1∧. . .∧θn). Then: •If NΘdoes not contain any satisfiable δ-clause, then Θis universally valid, and the process stops1. •Else, Nδ Θis obtained, and: –If ♦∈Nδ Θ, then Θis not satisfiable, and the process stops2. –Else, Step 2: Observation Analysis. Let Obe the δ-clausal form of φ. Then: •If Odoes not contain any satisfiable δ-clause, then φis not satisfiable, and the process stops3. •Else, Oδis obtained, and: 1When the theory Θ is universally valid, hΘ, φicannot have abductive solutions in the sense of definition 2, because every δ-clause Σ which satisfies (3) does not satisfy (5). 2Now, hΘ, φicannot be an abductive problem, because Θ φ(and also Θ ¬φ). 3In this case, every Θ verifies Θ ¬φ, so hΘ, φiis not an abductive problem. Abductive Reasoning Through δ-Resolution 355 –If ♦∈Oδ, then φis universally valid, and the process stops4. –Else, Step 3: Refutation search. If for every δ-clause Σ∈Oδthere is a Σ0⊆Σ such that Σ0∈Nδ Θ, then Θ¬φ, and the process stops. Else, Step 4: Explanations search. From Nδ Θand Oδ,(Nδ Θ∪Oδ)and then (Nδ Θ∪ Oδ)δare obtained. Then, •If ♦∈(Nδ Θ∪Oδ)δ, then Θφand the process stops. •Else, hΘ, φiis an abductive problem. The output is, Abd (Θ, φ) = Nδ Θ∪Oδδ−Nδ Θ∪Oδ Corollary 26 (Soundness of the abductive process) For every Θ⊂ Lp and φ∈ Lp, the abductive process described in algorithm 25 for hΘ, φiis sound. Proof: For a given formula α∈ Lpwith Aas its δ-clausal form, ♦∈Aδ iff α. Also, αis not satisfiable iff Ais not satisfiable, what means, given definitions 6 and 7, that there is no satisfiable δ-clause in A. With this observation, the proof of the soundness of steps 1 and 2 of algorithm 25 is direct. Step 3 is a consequence of corollary 24. For step 4, if ♦∈(Nδ Θ∪Oδ)δ, then Nδ Θ∪Oδis universally valid (theorem 13). But this is the δ-clausal form of ¬(θ1∧. . . ∧θn)∨φ, so ¬(θ1∧. . . ∧θn)∨φ, what is equivalent to Θ φ. Else, the way that step 4 follows to construct the set Abd(Θ, φ) is correct by corollary 23.  5 Comments Let us finish with some remarks about the δ-resolution calculus. We have defined it as an abductive calculus, due to its duality with respect to the standard resolution calculus. The duality between deduction and abduction is commonly pointed out in the abductive literature, sometimes related to the duality between forward and backward reasoning (abduction is usually characterized as backward deduction). We find suggestive that the δ-resolu- tion calculus catches this duality. It is possible to extend the δ-resolution calculus to first order logic, by using Herbrandization [2] (dual to Skolemization) and reversed skolemization [4]. The undecidability problem appears, but it is possible to restrict the abductive search to finite domains, in a similar way to [5]. 4Now, Θ φ