=Paper=
{{Paper
|id=Vol-3193/short4GDE
|storemode=property
|title=A Query Evaluation Method for ASP with Abduction
|pdfUrl=https://ceur-ws.org/Vol-3193/short4GDE.pdf
|volume=Vol-3193
|authors=Ken Satoh
|dblpUrl=https://dblp.org/rec/conf/iclp/Satoh22
}}
==A Query Evaluation Method for ASP with Abduction==
https://ceur-ws.org/Vol-3193/short4GDE.pdf
A Query Evaluation Method for ASP with Abduction
Ken Satoh
National Institute of Informatics, Tokyo, Japan
Abstract
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.
Keywords
Logic Programming, Abduction, Topdown Proof Procedure
1. Introduction
In this paper, we present a query evaluation method that is correct for every consistent1
abductive framework proposed in [Kakas90a]. If our procedure answers “yes”, then there is a
set of hypotheses which satisfies a query. If our procedure answers “no”, then there is no set of
hypotheses which satisfies a query.
Our procedure can be regarded as a correction of Kakas and Mancarella’s proce-
dure [Kakas90b] in the following two points.
Forward evaluation of rules:
It is important to use integrity constraints to exclude undesirable results from abduction.
However, their procedure manipulates a class of integrity constraints in which there is at least
one abducible predicate in each integrity constraint.
Check for Implicit Deletions:
We check consistency for “implicit deletions” first observed by Sadri and Kowalski [Sadri88].
The proposed methods [Kakas90b] do not check consistency of implicit deletion. We believe
that this lack of check is a major culprit of incorrectness in these methods. Inversely, we check
the implicit deletion in our procedure.
For example, consider the following program with an abducible predicate 𝑛𝑜𝑟𝑚𝑎𝑙_𝑏𝑎𝑟𝑏𝑒𝑟† 2 .
2nd Workshop on Goal-directed Execution of Answer Set Programs (GDE’22), August 1, 2022
This paper is an extended abstract of a paper with the title “A Query Evaluation Method for Abductive Logic
Programming” that appeared in the Proceedings of the Joint International Conference and Symposium on Logic
Programming (JICSLP’92), pp. 671 – 685.
" ksatoh@nii.ac.jp (K. Satoh)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings CEUR Workshop Proceedings (CEUR-WS.org)
http://ceur-ws.org
ISSN 1613-0073
1
Consistency of an abductive framework means that there is a generalized stable model for the framework.
2
∼ expresses negation as failure
𝑚𝑎𝑛(𝑛𝑜𝑒𝑙) ← (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.
2. A Semantics of Abductive Framework
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 𝑀 iff 𝑀 =
𝑀
𝑚𝑖𝑛(Π𝑀𝑇 ) 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 range-
restricted, 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 Θ.
3. Query Evaluation for Abduction
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 sufficient 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 sufficient 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.
4
Note 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 termi-
nates 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 gener-
alized 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 ∼𝑝.
4. Conclusion
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.
Acknowledgments
This work was supported by JSPS KAKENHI Grant Numbers, JP17H06103 and JP19H05470 and
JST, AIP Trilateral AI Research, Grant Number JPMJCR20G4.
References
[Kakas90a] Kakas, A. C., Mancarella, P., Generalized Stable Models: A Semantics for Abduction,
Proc. of ECAI’90, pp. 385 – 391 (1990).
[Kakas90b] Kakas, A. C., Mancarella, P., On the Relation between Truth Maintenance and
Abduction, Proc. of PRICAI’90, pp. 438 – 443 (1990).
[Sadri88] Sadri, F., Kowalski, R., A Theorem-Proving Approach to Database Integrity, Founda-
tions of Deductive Database and Logic Programming, (J. Minker, Ed.), Morgan Kaufmann
Publishers, pp. 313 – 362 (1988).
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 (𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛)
Figure 1: The definition of 𝑑𝑒𝑟𝑖𝑣𝑒 and 𝑙𝑖𝑡𝑒𝑟𝑎𝑙_𝑐𝑜𝑛
𝑟𝑢𝑙𝑒_𝑐𝑜𝑛(𝑅, Δ) 𝑅: 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 𝑑𝑒𝑙𝑒𝑡𝑒𝑑_𝑐𝑜𝑛