In this paper, we present a goal-directed proof procedure for ASP with abduction. Our proposed procedure in this paper is correct for any consistent abductive framework proposed in [Kakas90a]. In other words, if the procedure succeeds, there is a set of hypotheses which satisfies a query, and if the procedure finitely fails, there is no such set. If we do not consider abducibles, this procedure is a goal-directed proof procedure for ASP as well.
() ← (1) () ← (2) ℎ(, ) ← (), ∼ ℎ(, ) (3) ℎ(, ) ← (), _†() (4) ℎ(, ) ← (), ∼ _†() (5) Since () is true from (2), ℎ(, ) will be derived by using Kakas and Mancarella’s proof procedure and assuming ∼ _†() in (5). However, actually, there is no generalized stable model which satsifies ℎ(, ). We solve this problem by using the above techniques.
We mainly follow the definition of abductive framework in [ Kakas90a], but we modify it slightly for notational conveniences. Firstly, we define a rule and an integrity constraint. Definition 1. Let be an atom, and 1, ..., ( ≥ 0) be literals each of which is an atom or a negated atom of the form ∼ . A rule is of the form: ←
1, 2, ..., .
We call the head of the rule and 1, ..., the body of the rule. Let be a rule. ℎ(), () and () denote the head of , the set of literals in the body of and the set of positive literals in () respectively.
Definition 2. Let 1, ..., ( ≥ 0) be literals. An integrity constraint is of the form: ⊥ ←
1, 2, ..., .
For a given program (with integrity constraints), we define a stable model (in other words, answer set) as follows.
Definition 3. Let be a logic program and Π be a set of ground rules obtained by replacing all variables in each rule in by every element of its Herbrand universe. Let be a set of ground atoms from Π and Π be the following (possibly infinite) program.
Π = { ← 1, ..., | ← 1, ..., , ∼ 1, ..., ∼ ∈ Π
and ̸∈ for each = 1, ..., .} Let (Π ) be the least model of Π . A stable model for a logic program is if = (Π ) and ⊥ ̸∈ .
This definition gives a stable model of which satisfies all integrity constraints. We say that is consistent if there exists a stable model for .
Now, we define an abductive framework.
Definition 4. An abductive framework is a pair ⟨, ⟩ where is a set of predicate symbols, called abducible predicates and is a set of rules each of whose head is not in . We call a set of all ground atoms for predicates in abducibles. As pointed out in [Kakas90a], we can translate a program which includes a definition of abducibles to an equivalent framework that satisfies the above requirement. Moreover, we impose an abductive framework to be rangerestricted, that is, any variable in a rule of a program must occur in non-abducible positive literals of the rule.
Now, we define a semantics of an abductive framework.
Definition 5. Let ⟨, ⟩ be an abductive framework and Θ be a set of abducibles. A generalized stable model (Θ) is a stable model of ∪ { ← | ∈ Θ}.
We say that ⟨, ⟩ is consistent if there exists a generalized stable model (Θ) for some Θ.
Before showing our query evaluation method, we need the following definitions. Let be a literal. Then, denotes the complement of 3 Definition 6. Let be a logic program. A set of resolvents w.r.t. a ground literal and , (, ) is the following set of rules: (, ) = {(⊥ ← 1, ..., ) | is negative and
← 1, ..., ∈ and = by a ground substitution }∪ {( ← 1, ..., − 1, +1, ..., ) |
← 1, ..., ∈ and = by a ground substitution } The first set of resolvents are for negation as failure and the second set of resolvents corresponds with “forward” evaluation of the rule introduced in [Sadri88].
Definition 7. Let be a logic program. A set of deleted rules w.r.t. a ground literal and , (, ), is the following set of rules: (, ) = {( ← 1, ..., ) |
← 1, ..., ∈ and = by a ground substitution }
Our query evaluation procedure consists of 4 subprocedures, (, Δ), _(, Δ), _(, Δ) and _(, Δ) where is a non-abducible atom and Δ is a set of ground literals already assumed and is a ground literal and is a rule.
(, Δ) returns a ground substitution for the variables in and a set of ground literals. This set of ground literals is a union of Δ and literals newly assumed during execution of the subprocedure. Other subprocedures return a set of ground literals.
The subprocedures have a select operation and a fail operation. The select operation expresses a nondeterministic choice among alternatives. The fail operation expresses immediate termination of an execution with failure. Therefore, a subprocedure succeeds when its inner calls of subprocedures do not encounter fail. We say a subprocedure succeeds with ( and) Δ when the subprocedure successfully returns ( and) Δ.
The informal specification of the 4 subprocedures is as follows.
3 =∼ for a positive literal , and ∼ = for a negative literal ∼ . 1. (, Δ) searches a rule of in a program whose body can be made true with a ground substitution under a set of assumptions Δ. To show that every literal in the body can be made true, we call for non-abducible positive literals in the body. Then, we check the consistency of other literals in the body with and Δ. Note that because of the range-restrictedness, other literals in become ground after all the calls of for non-abducible positive literals. 2. _(, Δ) checks the consistency of a ground literal with and Δ. To show the consistency for assuming , we add to Δ; then, we check the consistency of resolvents and deleted rules w.r.t. and . 3. _(, Δ) checks the consistency of a rule with and Δ. If is not ground, we must check the consistency for ground instances of . But it is suficient to consider every ground instance in Ω ∪{}. We can prove the consistency by showing that either a literal in ( ) can be falsified or ( ) can be made true and ℎ( ) consistent.
This procedure can also be used to check integrity for rule addition. 4. _(, Δ) checks if a deletion of does not cause any contradictions with and Δ. To show the consistency of the implicit deletion of , it is suficient to prove that the head of every ground instance in Ω 4 can be made either true or false. Thanks to the range-restrictedness, we can compute all ground instances of a rule (if they are finite) in Ω (or Ω ∪{}). For this, we compute every SLD derivation of a query which consists of all non-abducible positive literals in () to the abducible-and-negation-removed program − (or ( ∪ {})− ).
Please see the details of each subprocedure at Figure 1 and Figure 2 in Appendix. In Figure 1, denotes empty substitution and expresses a composition of two substitutions and . Also, we denote a set of non-abducible positive literals, non-abducible negative literals, and abducibles (either negative or positive) in a rule as (), () and ().
If we remove _ and do not consider resolvents obtained with “forward” evaluation of the rule, then this procedure coincides with that of Kakas and Mancarella [Kakas90a]. That is, our procedure is obtained by augmenting their procedure with an integrity constraint checking in a bottom-up manner and with an implicit deletion checking.
We can show the following theorems for correctness of successful derivation, consistency check for addition of a rule and finite failure.
Theorem 1. Let ⟨, ⟩ be a consistent abductive framework. Suppose (, {}) succeeds with (, Δ). Then, there exists a generalized stable model (Θ) for such that Θ includes all positive abducibles in Δ and (Θ) |= .
This theorem means that if the procedure (, {}) answers “yes” with (, Δ), then there is a generalized stable model which satisfies . However, we cannot say in general that we make true only with positive abducibles in Δ, because there might be some hypotheses which are irrelevant to a query but which we must assume to get consistency.
The following theorem states correctness for consistency for addition of a rule.
4Note that Ω ∪{} = Ω since is an instance of a rule in .
Theorem 2. Let ⟨, ⟩ be a consistent abductive framework. Suppose _(, {}) succeeds, then ⟨ ∪ , ⟩ is a consistent abductive framework.
This means that this procedure can be used to guarantee the existence of a generalized stable model for a given abductive framework ⟨, ⟩ if iterative calls of _ succeed from ⟨{}, ⟩ by adding each rule in .
The following is a theorem related to correctness for finite failure.
Theorem 3. Let ⟨, ⟩ be an abductive framework. Suppose that every selection of rules terminates for (, {}) with either success or failure. If there exists a generalized stable model (Θ) for ⟨, ⟩ and a ground substitution such that (Θ) |= , then there is a selection of rules such that (, {}) succeeds with (, Δ) where Θ includes all positive abducibles in Δ. This theorem means that if we can search exhaustively in selecting the rules and there is a generalized stable model which satisfies a query, then the procedure always answers “yes”.
With this theorem, we obtain the following corollary for a finite failure.
Corollary 1. Let ⟨, ⟩ be an abductive framework. If (, {}) fails, then for every generalized stable model (Θ) for ⟨, ⟩ and for every ground substitution , (Θ) ̸|= . When the procedure (, {}) answers “no”, there is no generalized stable model which satisfies the query. Also, this corollary means that we can use a finite failure to check if the negation of a ground literal is true in all generalized stable models since finite failure of (, {}) means that every generalized stable model satisfies ∼ .
In this paper, we propose a query evaluation method for an abductive framework. Our procedure can be regarded as an extension of the procedure of Kakas and Mancarella by augmenting forward evaluation of rules and consistency check for implicit deletion.
This work was supported by JSPS KAKENHI Grant Numbers, JP17H06103 and JP19H05470 and JST, AIP Trilateral AI Research, Grant Number JPMJCR20G4.
Appendix: Topdown Proof Procedure (, Δ) : a non-abducible atom; Δ: a set of literals begin if is ground and ∈ Δ then return (, Δ) elseif is ground and ∼ ∈ Δ then fail else begin select ∈ s.t. ℎ() and are unifiable with an mgu if such a rule is not found then fail Δ0 := Δ, 0 := , 0 := ( ), := 0 while ̸= {} do begin take a literal in if (, Δ) succeeds with ( , Δ+1)
then +1 := , +1 := ( − { }) , := + 1 and continue end := for every ∈ ( ) ∪ ( ) do begin if _(, Δ) succeeds with Δ+1
then := + 1 and continue end if _(, Δ) succeeds with Δ′ then return (, Δ′) end end () _(, Δ) : a ground literal; Δ: a set of literals begin if ∈ Δ then return Δ elseif = ⊥ or ∈ Δ then fail else begin Δ0 := {} ∪ Δ, := 0 for every ∈ (, ) do if _(, Δ) succeeds with Δ+1
then := + 1 and continue for every ∈ (, ) do if _(, Δ) succeeds with Δ+1
then := + 1 and continue end return Δ end (_) _(, Δ) : a rule; Δ: a set of literals begin Δ0 := Δ, := 0 for every ground rule ∈ Ω ∪{} do begin select (a) or (b) (a) select ∈ ( ) if ∈ ( ) ∪ ( ) and _(, Δ) succeeds with Δ+1
then := + 1 and continue elseif ∈ ( ) and (, Δ) succeeds with (, Δ+1)
then := + 1 and continue (b) Δ0 := Δ, := 0 for every ∈ ( ) do begin if ∈ ( ) and (, Δ) succeeds with (, Δ+1) then := + 1 and continue elseif ∈ ( ) ∪ ( ) and _(, Δ) succeeds with Δ
+1 then := + 1 and continue end if _(ℎ( ), Δ) succeeds with Δ+1
then := + 1 and continue end return Δ end (_) _(, Δ) : a rule; Δ: a set of literals begin Δ0 := Δ, := 0 for every ground rule ∈ Ω do begin select (a) or (b) (a) if (ℎ( ), Δ) succeeds with (, Δ+1)
then := + 1 and continue (b) if _(∼ ℎ( ), Δ) succeeds with Δ+1
then := + 1 and continue end return Δ end (_) Figure 2: The definition of _ and _