SLT-Resolution for the Well-Founded Semantics
Yi-Dong Shen∗
Department of Computer Science, Chongqing University, Chongqing 400044, P.R.China

arXiv:cs/0002016v3 [] 2 Mar 2001

Email: ydshen@cs.ualberta.ca

Li-Yan Yuan and Jia-Huai You
Department of Computing Science, University of Alberta, Edmonton, Alberta, Canada T6G 2H1
Email: {yuan, you}@cs.ualberta.ca

Abstract
Global SLS-resolution and SLG-resolution are two representative mechanisms for
top-down evaluation of the well-founded semantics of general logic programs. Global
SLS-resolution is linear for query evaluation but suffers from infinite loops and redundant computations. In contrast, SLG-resolution resolves infinite loops and redundant
computations by means of tabling, but it is not linear. The principal disadvantage
of a non-linear approach is that it cannot be implemented using a simple, efficient
stack-based memory structure nor can it be easily extended to handle some strictly
sequential operators such as cuts in Prolog.
In this paper, we present a linear tabling method, called SLT-resolution, for topdown evaluation of the well-founded semantics. SLT-resolution is a substantial extension of SLDNF-resolution with tabling. Its main features include: (1) It resolves
infinite loops and redundant computations while preserving the linearity. (2) It is terminating, and sound and complete w.r.t. the well-founded semantics for programs with
the bounded-term-size property with non-floundering queries. Its time complexity is
comparable with SLG-resolution and polynomial for function-free logic programs. (3)
Because of its linearity for query evaluation, SLT-resolution bridges the gap between
the well-founded semantics and standard Prolog implementation techniques. It can be
implemented by an extension to any existing Prolog abstract machines such as WAM
or ATOAM.
Keywords: Well-founded semantics, procedural semantics, linear tabling, Global SLSresolution, SLG-resolution, SLT-resolution.
∗

Work completed during a visit at Department of Computing Science, University of Alberta, Canada.

1

1

Introduction

The central component of existing logic programming systems is a refutation procedure,
which is based on the resolution rule created by Robinson [21]. The first such refutation
procedure, called SLD-resolution, was introduced by Kowalski [13, 31], and further formalized
by Apt and Van Emden [1]. SLD-resolution is only suitable for positive logic programs, i.e.
programs without negation. Clark [8] extended SLD-resolution to SLDNF-resolution by
introducing the negation as finite failure rule, which is used to infer negative information.
SLDNF-resolution is suitable for general logic programs, by which a ground negative literal
¬A succeeds if A finitely fails, and fails if A succeeds.
As an operational/procedural semantics of logic programs, SLDNF-resolution has many
advantages, among the most important of which is its linearity of derivations. Let G0 ⇒C1 ,θ1
G1 ⇒ ... ⇒Ci ,θi Gi be a derivation with G0 the top goal and Gi the latest generated goal.
A resolution is said to be linear for query evaluation if when applying the most widely used
depth-first search rule, it makes the next derivation step either by expanding Gi using a
program clause (or a tabled answer), which yields Gi ⇒Ci+1 ,θi+1 Gi+1 , or by expanding Gi−1
via backtracking.1 It is with such linearity that SLDNF-resolution can be realized easily and
efficiently using a simple stack-based memory structure [36, 38]. This has been sufficiently
demonstrated by Prolog, the first and yet the most popular logic programming language
which implements SLDNF-resolution.
However, SLDNF-resolution suffers from two serious problems. One is that the declarative semantics it relies on, i.e. the completion of programs [8], incurs some anomalies (see
[15, 29] for a detailed discussion); and the other is that it may generate infinite loops and a
large amount of redundant sub-derivations [2, 9, 35].
The first problem with SLDNF-resolution has been perfectly settled by the discovery of
the well-founded semantics [33].2 Two representative methods were then proposed for topdown evaluation of such a new semantics: Global SLS-resolution [18, 22] and SLG-resolution
[6, 7].
Global SLS-resolution is a direct extension of SLDNF-resolution. It overcomes the semantic anomalies of SLDNF-resolution by treating infinite derivations as failed and infinite
recursions through negation as undefined. Like SLDNF-resolution, it is linear for query
evaluation. However, it inherits from SLDNF-resolution the problem of infinite loops and
redundant computations. Therefore, as the authors themselves pointed out, Global SLSresolution can be considered as a theoretical construct [18] and is not effective in general
[22].
SLG-resolution (similarly, Tabulated SLS-resolution [4]) is a tabling mechanism for top1

The concept of “linear” here is different from the one used for SL-resolution [12].
Some other important semantics, such as the stable model semantics [11], are also proposed. However,
for the purpose of query evaluation the well-founded semantics seems to be the most natural and robust.
2

2

down evaluation of the well-founded semantics. The main idea of tabling is to store intermediate results of relevant subgoals and then use them to solve variants of the subgoals whenever
needed. With tabling no variant subgoals will be recomputed by applying the same set of
program clauses, so infinite loops can be avoided and redundant computations be substantially reduced [4, 7, 30, 35, 37]. Like all other existing tabling mechanisms, SLG-resolution
adopts the solution-lookup mode. That is, all nodes in a search tree/forest are partitioned
into two subsets, solution nodes and lookup nodes. Solution nodes produce child nodes only
using program clauses, whereas lookup nodes produce child nodes only using answers in the
tables. As an illustration, consider the derivation p(X) ⇒Cp1 ,θ1 q(X) ⇒Cq1 ,θ2 p(Y ). Assume
that so far no answers of p(X) have been derived (i.e., currently the table for p(X) is empty).
Since p(Y ) is a variant of p(X) and thus a lookup node, the next derivation step is to expand
p(X) against a program clause, instead of expanding the latest generated goal p(Y ). Apparently, such kind of resolutions is not linear for query evaluation. As a result, SLG-resolution
cannot be implemented using a simple, efficient stack-based memory structure nor can it be
easily extended to handle some strictly sequential operators such as cuts in Prolog because
the sequentiality of these operators fully depends on the linearity of derivations.3 This has
been evidenced by the fact that XSB, the best known state-of-the-art tabling system that
implements SLG-resolution, disallows clauses like
p(.) ← ..., t(.), !, ...
because the tabled predicate t occurs in the scope of a cut [23, 24, 25].
One interesting question then arises: Can we have a linear tabling method for top-down
evaluation of the well-founded semantics of general logic programs, which resolves infinite
loops and redundant computations (like SLG-resolution) without sacrificing the linearity of
SLDNF-resolution (like Global SLS-resolution)? In this paper, we give a positive answer to
this question by developing a new tabling mechanism, called SLT-resolution. SLT-resolution
is a substantial extension of SLDNF-resolution with tabling. Its main features are as follows.
• SLT-resolution is based on finite SLT-trees. The construction of SLT-trees can be
viewed as that of SLDNF-trees with an enhancement of some loop handling mechanisms. Consider again the derivation p(X) ⇒Cp1 ,θ1 q(X) ⇒Cq1 ,θ2 p(Y ). Note that the
derivation has gone into a loop since the proof of p(X) needs the proof of p(Y ), a variant of p(X). By SLDNF- or Global SLS-resolution, P (Y ) will be expanded using the
same set of program clauses as p(X). Obviously, this will lead to an infinite loop of the
form p(X) ⇒Cp1 ...p(Y ) ⇒Cp1 ...p(Z) ⇒Cp1 ... In contrast, SLT-resolution will break
the loop by disallowing p(Y ) to use the clause Cp1 that has been used by p(X). As a
result, SLT-trees are guaranteed to be finite for programs with the bounded-term-size
property.
• SLT-resolution makes use of tabling to reduce redundant computations, but is linear
3

It is well known that cuts are indispensable in real world programming practices.

3

for query evaluation. Unlike SLG-resolution and all other existing top-down tabling
methods, SLT-resolution does not distinguish between solution and lookup nodes. All
nodes will be expanded by applying existing answers in tables, followed by program
clauses. For instance, in the above example derivation, since currently there is no
tabled answer available to p(Y ), p(Y ) will be expanded using some program clauses.
If no program clauses are available to p(Y ), SLT-resolution would move back to q(X)
(assume using a depth-first control strategy). This shows that SLT-resolution is linear
for query evaluation. When SLT-resolution moves back to p(X), all program clauses
that have been used by p(Y ) will no longer be used by p(X). This avoids redundant
computations.
• SLT-resolution is terminating, and sound and complete w.r.t. the well-founded semantics for any programs with the bounded-term-size property with non-floundering
queries. Moreover, its time complexity is comparable with SLG-resolution and polynomial for function-free logic programs.
• Because of its linearity for query evaluation, SLT-resolution can be implemented by
an extension to any existing Prolog abstract machines such as WAM [36] or ATOAM
[38]. This differs significantly from non-linear resolutions such as SLG-resolution since
their derivations cannot be organized using a stack-based memory structure, which is
the key to the Prolog implementation.

1.1

Notation and Terminology

We present our notation and review some standard terminology of logic programs [15].
Variables begin with a capital letter, and predicate, function and constant symbols with
~ we denote an atom with the list
a lower case letter. Let p be a predicate symbol. By p(X)
~ of variables. Let S = {A1 , ..., An } be a set of atoms. By ¬.S we denote the complement
X
{¬A1 , ..., ¬An } of S.
Definition 1.1 A general logic program (program for short) is a finite set of (program)
clauses of the form
A ← L1 , ..., Ln
where A is an atom and Li s are literals. A is called the head and L1 , ..., Ln is called the
body of the clause. If a program has no clause with negative literals in its body, it is called
a positive program.
Definition 1.2 ([22]) Let P be a program and p̄, f¯ and c̄ be a predicate symbol, function
symbol and constant symbol respectively, none of which appears in P . The augmented
program P̄ = P ∪ {p̄(f¯(c̄))}.
4

Definition 1.3 A goal is a headless clause ← L1 , ..., Ln where each Li is called a subgoal.
When n = 0, the “←” symbol is omitted. A computation rule (or selection rule) is a rule for
selecting one subgoal from a goal.
Let Gj =← L1 , ..., Li , ..., Ln be a goal with Li a positive subgoal. Let Cl = L ← F1 , ..., Fm
be a clause such that Lθ = Li θ where θ is an mgu (i.e. most general unifier). The resolvent
of Gj and Cl on Li is the goal Gk =← (L1 , ..., Li−1 , F1 , ..., Fm , Li+1 , ..., Ln )θ. In this case, we
say that the proof of Gj is reduced to the proof of Gk .
The initial goal, G0 =← L1 , ..., Ln , is called a top goal. Without loss of generality, we
shall assume throughout the paper that a top goal consists only of one atom (i.e. n = 1
and L1 is a positive literal). Moreover, we assume that the same computation rule R always
selects subgoals at the same position in any goals. For instance, if Li in the above goal Gj is
selected by R, then F1 θ in Gk will be selected by R since Li and F1 θ are at the same position
in their respective goals.
Definition 1.4 Let P be a program. The Herbrand universe of P is the set of ground
terms that use the function symbols and constants in P . (If there is no constant in P , then
an arbitrary one is added.) The Herbrand base of P is the set of ground atoms formed by
predicates in P whose arguments are in the Herbrand universe. By ∃(Q) and ∀(Q) we denote
respectively the existential and universal closure of Q over the Herbrand universe.

Definition 1.5 A Herbrand instantiated clause of a program P is a ground instance of some
clause C in P that is obtained by replacing all variables in C with some terms in the Herbrand
universe of P . The Herbrand instantiation of P is the set of all Herbrand instantiated clauses
of P .

Definition 1.6 Let P be a program and HP its Herbrand base. A partial interpretation I of P is a set {A1 , ..., Am , ¬B1 , ..., ¬Bn } such that {A1 , ..., Am , B1 , ..., Bn } ⊆ HP and
{A1 , ..., Am } ∩ {B1 , ..., Bn } = ∅. We use I + and I − to refer to {A1 , ..., Am } and {B1 , ..., Bn },
respectively.
Definition 1.7 By a variant of a literal L we mean a literal L′ that is the same as L up to
variable renaming. (Note that L is a variant of itself.)
Finally, a substitution α is more general than a substitution β if there exists a substitution γ such that β = αγ. Note that α is more general than itself because α = αε where ε is
the identity substitution [15].

5

2

The Well-Founded Semantics

In this section we review the definition of the well-founded semantics of logic programs. We
also present a new constructive definition of the greatest unfounded set of a program, which
has technical advantages for the proof of our results.
Definition 2.1 ([22, 33]) Let P be a program and HP its Herbrand base. Let I be a
partial interpretation. U ⊆ HP is an unfounded set of P w.r.t. I if each atom A ∈ U
satisfies the following condition: For each Herbrand instantiated clause C of P whose head
is A, at least one of the following holds:
1. The complement of some literal in the body of C is in I.
2. Some positive literal in the body of C is in U.
The greatest unfounded set of P w.r.t. I, denoted UP (I), is the union of all sets that are
unfounded w.r.t. I.

Definition 2.2 ([22]) Define the following transformations:
• A ∈ TP (I) if and only if there is a Herbrand instantiated clause of P , A ← L1 , ..., Lm ,
such that all Li are in I.
• T̄P (I) = TP (I) ∪ I.
• MP (I) =

S∞

k=1

T̄Pk (I), where T̄P1 (I) = T̄P (I), and for any i > 1 T̄Pi (I) = T̄P (T̄Pi−1 (I)).

• UP (I) is the greatest unfounded set of P w.r.t. I, as in Definition 2.1.
• VP (I) = MP (I) ∪ ¬.UP (I).
Since TP (I) derives only positive literals, the following result is straightforward.
Lemma 2.1 ¬A ∈ MP (I) if and only if ¬A ∈ I.

Definition 2.3 ([22, 33]) Let α and β be countable ordinals. The partial interpretations
Iα are defined recursively by
1. For limit ordinal α, Iα =

β<α Iβ ,

S

where I0 = ∅.

2. For successor ordinal α + 1, Iα+1 = VP (Iα ).

6

The transfinite sequence Iα is monotonically increasing (i.e. Iβ ⊆ Iα if β ≤ α), so
there exists the first ordinal δ such that Iδ+1 = Iδ . This fixpoint partial interpretation,
denoted W F (P ), is called the well-founded model of P . Then for any A ∈ HP , A is true if
A ∈ W F (P ), false if ¬A ∈ W F (P ), and undefined otherwise.
Lemma 2.2 For any J ⊆ W F (P ), MP (J) ⊆ W F (P ) and ¬.UP (J) ⊆ W F (P ).
Proof: Let J ⊆ Im . Since Iα is monotonically increasing, MP (J) ⊆ Im+1 ⊆ W F (P ) and
¬.UP (J) ⊆ Im+1 ⊆ W F (P ). ✷
The following definition is adapted from [20].
Definition 2.4 P |I is obtained from the Herbrand instantiation PHP of P by
• first deleting all clauses with a literal in their bodies whose complement is in I,
• then deleting all negative literals in the remaining clauses.
Clearly P |I is a positive program. Note that for any partial interpretation I, MP (I) is
a partial interpretation that consists of I and all ground atoms that are iteratively derivable
from PHP and I. We observe that the greatest unfounded set UP (I) of P w.r.t. I can be
constructively defined based on MP (I) and P |MP (I).
Definition 2.5 Define the following two transformations:
• NP (I) = HP −
• OP (I) =

S∞

k=1

S∞

k=1

T̄Pk |MP (I) (MP (I)).

T̄Pk |MP (I) (MP (I)) − MP (I).

We will show that NP (I) = UP (I) (see Theorem 2.5). The following result is immediate.
Lemma 2.3 MP (I)+ , NP (I) and OP (I) are mutually disjoint and HP = MP (I)+ ∪ NP (I) ∪
OP (I).
From Definitions 2.4 and 2.5 it is easily seen that OP (I) = ∞
i=1 Si , which is generated
iteratively as follows: First, for each A ∈ S1 there must be a Herbrand instantiated clause
of P of the form
A ← B1 , ..., Bm , ¬D1 , ..., ¬Dn
(1)
S

where all Bi s and some ¬Dj s are in MP (I) and for the remaining ¬Dk s (not empty; otherwise
A ∈ MP (I)) neither Dk nor ¬Dk is in MP (I). Note that the proof of A can be reduced to
the proof of ¬Dk s given MP (I). Then for each A ∈ S2 there must be a clause like (1) above
where no Dj is in MP (I), some Bi s are in MP (I), and the remaining Bk s (not empty) are
in S1 . Continuing such process of reduction, for each A ∈ Sl+1 with l ≥ 1 there must be a
clause like (1) above where no Dj is in MP (I), some Bi s are in MP (I), and the remaining
S
Bk s (not empty) are in li=1 Si .
The following lemma shows a useful property of literals in OP (I).
7

Lemma 2.4 Given MP (I), the proof of any A ∈ OP (I) can be reduced to the proof of a set
of ground negative literals ¬Ej s where neither Ej nor ¬Ej is in MP (I).
Proof: Let OP (I) = ∞
i=1 Si . The lemma is proved by induction on Si . Obviously, it holds
for each A ∈ S1 . As inductive hypothesis, assume that the lemma holds for any A ∈ Si with
1 ≤ i ≤ l. We now prove that it holds for each A ∈ Sl+1 .
Let A ∈ Sl+1 . For convenience of presentation, in clause (1) above for A let {B1 , ..., Bf } ⊆
S
MP (I) (f < m), {Bf +1 , ..., Bm } ⊆ li=1 Si , {¬D1 , ..., ¬De } ⊆ MP (I) (e ≤ n), and for each
Dk ∈ {De+1 , ..., Dn } neither Dk nor ¬Dk is in MP (I). By the inductive hypothesis the proof
of Bf +1 , ..., Bm can be reduced to the proof of a set NS = {¬N1 , ..., ¬Nt } of negative literals
where neither Nj nor ¬Nj is in MP (I). So the proof of A can be reduced to the proof of
{¬N1 , ..., ¬Nt , ¬De+1 , ..., ¬Dn }. ✷
S

Theorem 2.5 NP (I) = UP (I).
Proof: Let A ∈ NP (I) and A ← B1 , ..., Bm , ¬D1 , ..., ¬Dn be a Herbrand instantiated clause
of P for A. By Definition 2.5, either some ¬Bi or Dj is in MP (I), or (when A ← B1 , ..., Bm
is in P |MP (I)) there exists some Bi such that neither Bi ∈ MP (I)+ nor Bi ∈ OP (I), i.e.
Bi ∈ NP (I) (see Lemma 2.3). By Definition 2.1, NP (I) is an unfounded set w.r.t. I, so
NP (I) ⊆ UP (I).
Assume, on the contrary, that there is an A ∈ UP (I) but A 6∈ NP (I). Since UP (I) ∩
MP (I)+ = ∅, A ∈ OP (I). So there exists a Herbrand instantiated clause C of P
A ← B1 , ..., Bm , ¬D1 , ..., ¬Dn
such that C does not satisfy point 1 of Definition 2.1 (since I ⊆ MP (I)) and
A ← B1 , ..., Bm
is in P |MP (I) where each Bi is either in MP (I)+ or in OP (I). Since A ∈ UP (I), by point 2
of Definition 2.1 some Bj ∈ UP (I) and thus Bj ∈ OP (I).
Repeating the above process leads to an infinite chain: the proof of A needs the proof
of Bj1 that needs the proof of Bj2 , and so on, where each Bji ∈ OP (I). Obviously, for no
Bji along the chain its proof can be reduced to a set of ground negative literals ¬Ej s where
neither Ej nor ¬Ej is in MP (I). This contradicts Lemma 2.4, so UP (I) ⊆ NP (I). ✷
Starting with I = ∅, we compute MP (I), followed by OP (I) and NP (I). By Lemma
2.2 and Theorem 2.5, each A ∈ MP (I)+ (resp. A ∈ NP (I)) is true (resp. false) under
the well-founded semantics. OP (I) is a set of temporarily undefined ground literals whose
truth values cannot be determined at this stage of transformations based on I. We then do
iterative computations by letting I = MP (I) ∪ ¬.NP (I) until we reach a fixpoint. This forms
the basis on which our operational procedure is designed for top-down computation of the
well-founded semantics.

8

3

SLT-Trees and SLT-Resolution

In this section, we define SLT-trees and SLT-resolution. Here “SLT” stands for “Linear
Tabulated resolution using a Selection/computation rule.”
Recall the familiar notion of a tree for describing the search space of a top-down proof
procedure. For convenience, a node in such a tree is represented by Ni : Gi , where Ni is the
node name and Gi is a goal labeling the node. Assume no two nodes have the same name.
Therefore, we can refer to nodes by their names.
Definition 3.1 ([26] with slight modification) An ancestor list ALA of pairs (Ni , Ai ),
where Ni is a node name and Ai is an atom, is associated with each subgoal A in a tree,
which is defined recursively as follows.
1. If A is at the root, then ALA = ∅ unless otherwise specified.
2. Let A be at node Ni+1 and Ni be its parent node. If A is copied or instantiated from
some subgoal A′ at Ni then ALA = ALA′ .
3. Let Ni : Gi be a node that contains a positive literal B. Let A be at node Ni+1 that
is obtained from Ni by resolving Gi against a clause B ′ ← L1 , ..., Ln on the literal B
with an mgu θ. If A is Lj θ for some 1 ≤ j ≤ n, then ALA = {(Ni , B)} ∪ ALB .
Apparently, for any subgoals A and B if A is in the ancestor list of B, i.e. ( , A) ∈ ALB ,
the proof of A needs the proof of B. Particularly, if ( , A) ∈ ALB and B is a variant of A,
the derivation goes into a loop. This leads to the following.
Definition 3.2 Let R be a computation rule and Ai and Ak be two subgoals that are
selected by R at nodes Ni and Nk , respectively. If (Ni , Ai ) ∈ ALAk , Ai (resp. Ni ) is called
an ancestor subgoal of Ak (resp. an ancestor node of Nk ). If Ai is both an ancestor subgoal
and a variant, i.e. an ancestor variant subgoal, of Ak , we say the derivation goes into a loop,
where Nk and all its ancestor nodes involved in the loop are called loop nodes and the clause
used by Ai to generate this loop is called a looping clause of Ak w.r.t. Ai . We say a node is
loop-dependent if it is a loop node or an ancestor node of some loop node. Nodes that are
not loop-dependent are loop-independent.
In tabulated resolutions, intermediate positive and negative (or alternatively, undefined)
answers of some subgoals will be stored in tables at some stages. Such answers are called
tabled answers. Let T Bf be a table that stores some ground negative answers; i.e. for each
A ∈ T Bf ¬A ∈ W F (P ). In addition, we introduce a special subgoal, u∗ , which is assumed
to occur in neither programs nor top goals. u∗ will be used to substitute for some ground
negative subgoals whose truth values are temporarily undefined. We now define SLT-trees.

9

Definition 3.3 (SLT-trees) Let P be a program, G0 a top goal, and R a computation
rule. Let T Bf be a set of ground atoms such that for each A ∈ T Bf ¬A ∈ W F (P ). The
SLT-tree TG0 for (P ∪ {G0 }, T Bf ) via R is a tree rooted at node N0 : G0 such that for any
node Ni : Gi in the tree with Gi =← L1 , ..., Ln :
1. If n = 0 then Ni is a success leaf, marked by ✷t .
2. If L1 = u∗ then Ni is a temporarily undefined leaf, marked by ✷u∗ .
3. Let Lj be a positive literal selected by R. Let CLj be the set of clauses in P whose
heads unify with Lj and LCLj be the set of looping clauses of Lj w.r.t. its ancestor
variant subgoals. If CLj − LCLj = ∅ then Ni is a failure leaf, marked by ✷f ; else the
children of Ni are obtained by resolving Gi with each of the clauses in CLj − LCLj over
the literal Lj .
4. Let Lj = ¬A be a negative literal selected by R. If A is not ground then Ni is a flounder
leaf, marked by ✷f l ; else if A is in T Bf then Ni has only one child that is labeled by the
goal ← L1 , ..., Lj−1 , Lj+1 , ..., Ln ; else build an SLT-tree T←A for (P ∪ {← A}, T Bf ) via
R, where the subgoal A at the root inherits the ancestor list ALLj of Lj . We consider
the following cases:
(a) If T←A has a success leaf then Ni is a failure leaf, marked by ✷f ;
(b) If T←A has no success leaf but a flounder leaf then Ni is a flounder leaf, marked
by ✷f l ;
(c) Otherwise, Ni has only one child that is labeled by the goal ← L1 , ..., Lj−1 , Lj+1 , ...,
Ln , u∗ if Ln 6= u∗ or ← L1 , ..., Lj−1 , Lj+1, ..., Ln if Ln = u∗ .
In an SLT-tree, there may be four types of leaves: success leaves ✷t , failure leaves ✷f ,
temporarily undefined leaves ✷u∗ , and flounder leaves ✷f l . These leaves respectively represent successful, failed, (temporarily) undefined, and floundering derivations (see Definition
3.5). In this paper, we shall not discuss floundering − a situation where a non-ground negative literal is selected by a computation rule R (see [5, 10, 14, 19] for discussion on such
topic). Therefore, in the sequel we assume that no SLT-trees contain flounder leaves.
The construction of SLT-trees can be viewed as that of SLDNF-trees [8, 15] enhanced
with the following loop-handling mechanisms: (1) Loops are detected using ancestor lists of
subgoals. Positive loops occur within SLT-trees, whereas negative loops (i.e. loops through
negation) occur across SLT-trees (see point 4 of Definition 3.3, where the child SLT-tree
T←A is connected to its parent SLT-tree by letting A at the root of T←A inherit the ancestor
list ALLj of Lj ). (2) Loops are broken by disallowing subgoals to use looping clauses for
node expansion (see point 3 of Definition 3.3). This guarantees that SLT-trees are finite (see
Theorem 3.1). (3) Due to the exclusion of looping clauses, some answers may be missed in
10

an SLT-tree. Therefore, for any ground negative subgoal ¬A its answer (true or false) can
be definitely determined only when A is given to be false (i.e. A ∈ T Bf ) or the proof of A
via the SLT-tree T←A succeeds (i.e. T←A has a success leaf). Otherwise, ¬A is assumed to
be temporarily undefined and is replaced by u∗ (see point 4 of Definition 3.3). Note that
u∗ is only introduced to signify the existence of subgoals whose truth values are temporarily
undefined. Therefore, keeping one u∗ in a goal is enough for such a purpose (see point 4 (c)).
From point 2 of Definition 3.3 we see that goals with a subgoal u∗ cannot lead to a success
leaf. However, they may arrive at a failure leaf if one of the remaining subgoals fails.
For convenience, we use dotted edges to connect parent and child SLT-trees, so that
negative loops can be clearly identified (see Figure 1). Moreover, we refer to TG0 , the top SLTtree, along with all its descendant SLT-trees as a generalized SLT-tree for (P ∪ {G0 }, T Bf ),
denoted GTP,G0 (or simply GTG0 when no confusion would occur). Therefore, a path of a
generalized SLT-tree may come across several SLT-trees through dotted edges.
Example 3.1 Consider the following program and let G0 =← p(X) be the top goal.
P1 : p(X) ← q(X).
p(a).
q(X) ← ¬r.
q(X) ← w.
q(X) ← p(X).
r ← ¬s.
s ← ¬r.
w ← ¬w, v.

Cp 1
Cp 2
Cq 1
Cq 2
Cq 3
C r1
Cs 1
Cw 1

For convenience, let us choose the left-most computation rule and let T Bf = ∅. The generalized SLT-tree GT←p(X) for (P1 ∪ {← p(X)}, ∅) is shown in Figure 1,4 which consists of
five SLT-trees that are rooted at N0 , N6 , N8 , N10 and N16 , respectively. N2 and N15 are
success leaves because they are labeled by an empty goal. N10 , N16 and N17 are failure leaves
because they have no clauses to unify with except for the looping clauses Cr1 (for N10 ) and
Cw1 (for N16 ). N11 , N12 and N13 are temporarily undefined leaves because their goals consist
only of u∗ .
SLT-trees have some nice properties. Before proving those properties, we reproduce the
definition of bounded-term-size programs. The following definition is adapted from [32].
Definition 3.4 A program has the bounded-term-size property if there is a function f (n)
such that whenever a top goal G0 has no argument whose term size exceeds n, then no
subgoals and tabled answers in any generalized SLT-tree GTG0 have an argument whose
term size exceeds f (n).
4

For simplicity, in depicting SLT-trees we omit the “←” symbol in goals.

11

N0 : p(X)
Cp1

✟
✟
✙
✟

❍ Cp2
❍
❥
❍
✷t
N2 :

N1 : q(X)

❍ Cq3
Cq1 ✟✟
❥
❍
✙ Cq2 ❄ ❍
✟
N3 : ¬r

..
..
..

✙
N6 : r
Cr1
❄

❍

✙

N5 : p(X)

❍ Cp2
❍
❥
❍

Cw1
❄

❄

✷u∗ N14 .: ¬w, v
N13 : u∗ . . . .
❍
.
✙

✷f
N16 : w

N7 .: ¬s

.
..
..

N4 : w

✷t
N15 :

❍
❥
❍

✷f
N17 : v, u∗

❍
❥
❍
✷u∗
N12 : u∗

N8 : s
Cs1
❄

N9 : . ¬r
..
✙

✷f
N10 : r

.
..

❍
❍
❥
❍
✷u∗
N11 : u∗

Figure 1: The generalized SLT-tree GT←p(X) for (P1 ∪ {← p(X)}, ∅).
The following result shows that the construction of SLT-trees is always terminating for
programs with the bounded-term-size property.
Theorem 3.1 Let P be a program with the bounded-term-size property, G0 a top goal and
R a computation rule. The generalized SLT-tree GTG0 for (P ∪ {G0 }, T Bf ) via R is finite.
Proof: The bounded-term-size property guarantees that no term occurring on any path of
GTG0 can have size greater than f (n), where n is a bound on the size of terms in the top
goal G0 . Assume, on the contrary, that GTG0 is infinite. Then it must have an infinite path
because its branching factor (i.e. the average number of children of all nodes in the tree) is
bounded by the finite number of clauses in P . Since P has only a finite number of predicate,
function and constant symbols, some positive subgoal A0 selected by R must have infinitely
many variant descendants A1 , A2 , ..., Ai , ... on the path such that the proof of A0 needs the
proof of A1 that needs the proof of A2 , and so on. That is, Ai is an ancestor variant subgoal
of Aj for any 0 ≤ i < j. Let P have totally m clauses that can unify with A0 . Then by
point 3 of Definition 3.3, Am , when selected by R, will have no clause to unify with except
for the m looping clauses. That is, Am shoud be at a leaf, contradicting that it has variant
decendants on the path. ✷
Definition 3.5 Let TG0 be the SLT-tree for (P ∪ {G0 }, T Bf ). A successful (resp. failed or
undefined) branch of TG0 is a branch that ends at a success (resp. failure or temporarily
undefined) leaf. A correct answer substitution for G0 is given by θ = θ1 ...θn where the
θi s are the most general unifiers used at each step along a successful branch of TG0 . An
SLT-derivation of (P ∪ {G0 }, T Bf ) is a branch of TG0 .
Another principal property of SLT-trees is that correct answer substitutions for top goals
are sound w.r.t. the well-founded semantics.
12

Theorem 3.2 Let P be a program with the bounded-term-size property, G0 =← Q0 a top
goal, and TG0 the SLT-tree for (P ∪ {G0 }, T Bf ). For any correct answer substitution θ for
G0 in TG0 W F (P ) |= ∀(Q0 θ).
Proof: Let d be the depth of a successful branch. Without loss of generality, assume the
branch is of the form
N0 : G0 ⇒θ1 ,C1 N1 : G1 ⇒θ2 ,C2 ... ⇒θd−1 ,Cd−1 Nd−1 : Gd−1 ⇒θd ,Cd ✷t
where Gi =← Qi and θ = θ1 ...θd . We show, by induction on 0 ≤ k < d, W F (P ) |=
∀(Qk θk+1 ...θd ).
Let k = d−1. Since Nd is a success leaf, Gd−1 has only one literal, say L. If L is positive,
Cd must be a bodyless clause in P such that Lθd = Cd θd . In such a case, W F (P ) |= ∀(Cd ),
so that W F (P ) |= ∀(Qk θd ). Otherwise, L = ¬A is a ground negative literal. By point 4 of
Definition 3.3 A ∈ T Bf and thus W F (P ) |= ¬A. Therefore W F (P ) |= ∀(Qk θd ) with θd = ∅.
As induction hypothesis, assume that for 0 < k < d W F (P ) |= ∀(Qk θk+1 ...θd ). We now
prove W F (P ) |= ∀(Qk−1 θk θk+1 ...θd ).
Let Gk−1 =← L1 , ..., Ln with Li being the selected literal. If Li = ¬A is negative, A must
be ground and A ∈ T Bf (otherwise either Nk−1 is a flound leaf or a failure leaf, or Gk contains
a subgoal u∗ in which case Nk−1 will never lead to a success leaf). So W F (P ) |= (Li θk ) with
θk = ∅ and Gk =← L1 , ..., Li−1 , Li+1 , ..., Ln . By induction hypothesis we have
W F (P ) |= ∀(Qk θk+1 ...θd ) =⇒
W F (P ) |= ∀((L1 , ..., Li−1 , Li+1 , ..., Ln )θk+1 ...θd ) =⇒
W F (P ) |= ∀((L1 , ..., Li−1 , Li , Li+1 , ..., Ln )θk θk+1 ...θd ) =⇒
W F (P ) |= ∀(Qk−1 θk θk+1 ...θd ).
Otherwise, Li is positive. So there is a clause L′i ← B1 , ..., Bm in P with Li θk = L′i θk .
That is, Gk =← (L1 , ..., Li−1 , B1 , ..., Bm , Li+1 , ..., Ln )θk . Since Qk θk+1 ...θd is true in W F (P ),
(B1 , ..., Bm ) θk θk+1 ...θd is true in W F (P ). So L′i θk θk+1 ...θd is true in W F (P ). Therefore
W F (P ) |= ∀(Qk θk+1 ...θd ) =⇒
W F (P ) |= ∀((L1 , ..., Li−1 , B1 , ..., Bm , Li+1 , ..., Ln )θk θk+1 ...θd ) =⇒
W F (P ) |= ∀((L1 , ..., Li−1 , Li , Li+1 , ..., Ln )θk θk+1 ...θd ) =⇒
W F (P ) |= ∀(Qk−1 θk θk+1 ...θd ).
✷
SLT-trees provide a basis for us to develop a sound and complete method for computing
the well-founded semantics.
Observe that the concept of correct answer substitutions for a top goal G0 , defined in
Definition 3.5, can be extended to any goal Gi at node Ni in a generalized SLT-tree GTG0 .
This is done simply by adding a condition that the (sub-) branch starts at Ni . For instance,
in Figure 1 the branch that starts at N1 and ends at N15 yields a correct answer substitution
θ1 θ2 for the goal ← q(X) at N1 , where θ1 = {X1 /X} is the mgu of q(X) unifying with the
head of Cq3 and θ2 = {X/a} is the mgu of p(X) at N5 unifying with Cp2 . From the proof of

13

Theorem 3.2 it is easily seen that it applies to correct answer substitutions for any goals in
GTG0 .
Let Gi be a goal in GTG0 and Lj be the selected subgoal in Gi . Assume that Lj is
positive. The partial branches of GTG0 that are used to prove Lj constitute sub-derivations
for Lj . By Theorem 3.2, for any correct answer substitution θ built from a successful subderivation for Lj W F (P ) |= ∀(Lj θ). We refer to such intermediate results like Lj θ as tabled
positive answers.
Let T Bt0 consist of all tabled positive answers in GTG0 . Then P is equivalent to P 1 =
P ∪ T Bt0 w.r.t. the well-founded semantics. Due to the addition of tabled positive answers, a
new generalized SLT-tree GTG1 0 for (P 1 ∪ {G0 }, T Bf ) can be built with possibly more tabled
positive answers derived. Let T Bt1 consist of all tabled positive answers in GTG1 0 but not in
T Bt0 and P 2 = P 1 ∪ T Bt1 . Clearly P 2 is equivalent to P 1 w.r.t. the well-founded semantics.
Repeating this process we will generate a sequence of equivalent programs
P 1 , P 2, ..., P i , ...
where P i = P i−1 ∪ T Bti−1 and T Bti−1 consists of all tabled positive answers in GTGi−1
for
0
Si−2
i−1
k
(P ∪{G0 }, T Bf ) but not in k=0 T Bt , until we reach a fixpoint. This leads to the following
useful function.
Definition 3.6 Let P be a program, G0 a top goal and R a computation rule. Define
function SLT P (P, G0, R, T Bt , T Bf ) return a generalized SLT-tree GTG0
begin
Build a generalized SLT-tree GTG0 for (P ∪ {G0 }, T Bf ) via R;
NEWt collects all tabled positive answers in GTG0 but not in T Bt ;
if NEWt = ∅ then return GTG0
else return SLT P (P ∪ NEWt , G0 , R, T Bt ∪ NEWt , T Bf )
end
The following two theorems show that for positive programs with the bounded-termsize property, the function call SLT P (P, G0, R, ∅, ∅) is terminating, and sound and complete
w.r.t. the well-founded semantics. So we call it SLTP-resolution (i.e. SLT-resolution for
Positive programs).
Theorem 3.3 For positive programs with the bounded-term-size property SLTP-resolution
terminates in finite time.
Proof: The function call SLT P (P, G0, R, ∅, ∅) will generate a sequence of generalized SLTtrees
GTG0 0 , GTG1 0 , ..., GTGi 0 , ...
where GTG0 0 is the generalized SLT-tree for (P ∪{G0 }, ∅) via R, GTG1 0 is the generalized SLTtree for (P ∪ NEWt0 ∪ {G0 }, ∅) via R where NEWt0 consists of all tabled positive answers in
14

GTG0 0 , and GTGi 0 is the generalized SLT-tree for (P ∪NEWt0 ∪NEWt1 ∪...∪NEWti−1 ∪{G0 }, ∅)
S
k
via R where NEWti−1 consists of all tabled positive answers in GTGi−1
but not in i−2
k=0 NEWt .
0
Since by Theorem 3.1 the construction of each GTGi 0 is terminating, it suffices to prove that
there exists an i ≥ 0 such that NEWti = ∅.
Since P has the bounded-term-size property and has only a finite number of clauses, we
have only a finite number of subgoals in all generalized SLT-trees GTGi 0 s and any subgoal has
only a finite number of positive answers (up to variable renaming). Let N be the number of
all positive answers of all subgoals in all GTGi 0 s. Since before the fixpoint is reached, from
each GTGi 0 to GTGi+1
at least one new tabled positive answer to some subgoal will be derived,
0
there must exist an i ≤ N + 1 such that NEWti = ∅. ✷
Theorem 3.4 Let P be a positive program with the bounded-term-size property and G0 ← Q0
a top goal. Let GTG0 be the generalized SLT-tree returned by SLT P (P, G0, R, ∅, ∅). For any
(Herbrand) ground instance Q0 θ of Q0 W F (P ) |= Q0 θ if and only if there is a correct answer
substitution γ for G0 in GTG0 such that θ is an instance of γ.
The following lemma is required to prove this theorem.
Lemma 3.5 Let GTG0 0 , ..., GTGi 0 , ... be a sequence of generalized SLT-trees generated by SLT P (
P, G0 , R, ∅, T Bf ). For any 0 ≤ i < j, if θ is a correct answer substitution for G0 in GTGi 0 ,
so is it in GTGj 0 .
Proof: Assume that GTGi 0 and GTGj 0 are the generalized SLT-trees for (P ∪ NEWt ∪
{G0 }, T Bf ) and (P ∪ NEWt′ ∪ {G0 }, T Bf ), respectively. Then NEWt ⊆ NEWt′ . Let
N0 : G0 ⇒θ1 ,C1 N1 : G1 ⇒θ2 ,C2 ... ⇒θd−1 ,Cd−1 Nd−1 : Gd−1 ⇒θd ,Cd ✷t
be a successful branch in GTGi 0 . At each derivation step Nk−1 : Gk−1 ⇒θk ,Ck Nk : Gk , let
L be the selected literal in Gk−1. If L is a positive literal, Ck is either a clause in P or
a tabled positive answer in NEWt ; i.e. Ck ∈ P ∪ NEWt and thus Ck ∈ P ∪ NEWt′ . So
Nk−1 : Gk−1 ⇒θk ,Ck Nk : Gk must be in GTGj 0 . Otherwise, L = ¬A is a ground negative
literal. In this case A ∈ T Bf (otherwise either Nk−1 is a failure leaf or Gk contains a subgoal
u∗ in which case Nk−1 will never lead to a success leaf) and thus Nk−1 : Gk−1 ⇒θk ,Ck Nk : Gk
must be in GTGj 0 as well, where θk = ∅ and Ck = ¬A. Therefore, the above successful branch
will appear in GTGj 0 . ✷
Proof of Theorem 3.4: (⇐=) The function call SLT P (P, G0, R, ∅, ∅) will generate a
sequence of generalized SLT-trees
GTG0 0 , GTG1 0 , ..., GTGk 0 = GTG0
where GTG0 0 is the generalized SLT-tree for (P ∪{G0 }, ∅), GTG1 0 is the generalized SLT-tree for
(P 1 ∪{G0 }, ∅) with P 1 = P ∪NEWt0 , and GTG0 is the generalized SLT-tree for (P k ∪{G0 }, ∅)
with P k = P k−1 ∪ NEWtk−1 where NEWtk−1 is all tabled positive answers in GTGk−1
but not
0
Sk−2
i
i
in i=0 NEWt . Since NEWt s are sets of tabled positive answers, P is equivalent to P 1 that
15

is equivalent to P 2 that ... that is equivalent to P k under the well-founded semantics. By
Theorem 3.2, for any correct answer substitution γ for G0 in GTG0 W F (P k ) |= ∀(Q0 γ) and
thus W F (P ) |= ∀(Q0 γ).
(=⇒) Assume W F (P ) |= Q0 θ. By the definition of the well-founded semantics, there
must be a γ more general than θ such that Q0 γ can be derived by iteratively applying some
clauses in P . That is, we have a backward chain of the form
← Q0 ⇒θ1 ,C1 ← Q1 ⇒θ2 ,C2 ... ⇒θd−1 ,Cd−1 ← Qd−1 ⇒θd ,Cd ✷

(2)

where γ = θ1 ...θd and the Ci s are in P . We consider two cases.
Case 1: There is no loop or there are loops in (2) but no looping clauses are used. By
Definition 3.3 GTG0 0 must have a successful branch corresponding to (2). By Lemma 3.5
GTG0 contains such a branch, too.
Case 2: There are loops in (2) with looping clauses applied. With no loss in generality,
assume the backward chain (2) corresponds to the SLD-derivation shown in Figure 2, where
(1) The segments between N0 and Nl0 and between Nx0 and Nt contain no loops. For any
~ i ) is an ancestor variant subgoal of p(X
~ i+1 ). Obviously Cp is a looping
0 ≤ i < m p(X
j
~ i+1 ) w.r.t. p(X
~ i ).
clause of p(X
~ i ) reduces to the proof of (p(X
~ i+1 ), Bi+1 )
(2) For 0 ≤ i < m from Nli to Nli+1 the proof of p(X
~ i ), where each Bk (0 ≤ k ≤ m) is a set of subgoals.
with a substitution θi for p(X
(3) The sub-derivation between Nlm and Nxm contains no loops and yields an answer
~ m )γm to p(X
~ m ). The correct answer substitution γm for p(X
~ m ) is then applied to the
p(X
~ m−1 )γm γm−1 θm−1
remaining subgoals of Nlm (see node Nxm ), which leads to an answer p(X
~ m−1 ). Such process continues recursively until an answer p(X
~ 0 )γm ...γ0 θm−1 ...θ0
to p(X
~ 0 ) is produced at Nx0 .
to p(X
Since Cpj is a looping clause, the branch below Nl1 via Cpj will not occur in any SLT~ 0 )γm ...γ0 θm−1 ...θ0 to p(X
~ 0 ) will be
trees. We first prove that a variant of the answer p(X
derived and used as a tabled positive answer by SLTP-resolution.
~ 0 ) and p(X
~ m ) are variants, the sub-derivation between Nlm and Nxm will appear
Since p(X
directly below Nl0 via Cpj in GTG0 0 , without going through Nl1 . Thus a variant of the answer
~ m )γm to p(X
~ m ) will be derived and added to NEW 0 .
p(X
t
~
~
Since p(X0 ) and p(Xm−1 ) are variants, the sub-derivation between Nlm−1 and Nxm−1 ,
where the sub-derivation between Nlm and Nxm is replaced by directly using the tabled
~ m )γm in NEW 0 , will appear directly below Nl0 via Cp in GT 1 , without
positive answer p(X
j
G0
t
~ m−1 )γm γm−1 θm−1 to p(X
~ m−1 ) will be
going through Nl1 . Thus a variant of the answer p(X
derived and added to NEWt1 .
Continue the above process iteratively. After n (n ≤ m) iterations, a variant of the
~ 0 )γm ...γ0 θm−1 ...θ0 to p(X
~ 0 ) will be derived in GT n and added to NEW n .
answer p(X
G0
t
16

N0 : ← Q0

..
.

~0 ), B0
Nl0 : ← p(X
Cp
..❄ j
.

~1 ), B1 , B0 θ0
Nl1 : ← p(X
Cp
..❄ j
.

~ m ), Bm , Bm−1 θm−1 , ..., B1 θm−1 ...θ1 , B0 θm−1 ...θ0
Nlm : ← p(X
Cp
..❄ j
.

Nxm : ← Bm γm , Bm−1 γm θm−1 , ..., B1 γm θm−1 ...θ1 , B0 γm θm−1 ...θ0

..
.
Nx1 : ← B1 γm ...γ1 θm−1 ...θ1 , B0 γm ...γ1 θm−1 ...θ0

..
.
Nx0 : ← B0 γm ...γ0 θm−1 ...θ0

..
.
Nt : ✷

Figure 2: An SLD-derivation with loops.
Since by assumption there is no loop between N0 and Nl0 and between Nx0 and Nt ,
must contain a successful branch corresponding to Figure 2 except that the subderivation between Nl1 and Nx0 is replaced by directly applying the tabled positive answer
~ 0 )γm ...γ0 θm−1 ...θ0 . This branch has the same correct answer substitution for G0 as Figure
p(X
2 (up to variable renaming). By Lemma 3.5 GTG0 contains such a branch, too, so we conclude
the proof. ✷

GTGn+1
0

From the above proof it is easily seen that SLTP-resolution exhausts all tabled positive
answers for all selected positive subgoals in GTG0 . The following result is immediate.
Corollary 3.6 Let P be a positive program with the bounded-term-size property, G0 a top
goal, and GTG0 the generalized SLT-tree returned by SLT P (P, G0, R, ∅, ∅). Let T Bt consist
of all tabled positive answers in GTG0 . Then
1. Let A be a selected literal at some node in GTG0 . For any (Herbrand) ground instance
Aθ of A W F (P ) |= Aθ if and only if there is a tabled answer A′ in T Bt such that Aθ
is an instance of A′ .
2. Let Gi =← Qi be a goal in GTG0 . For any (Herbrand) ground instance Qi θ of Qi
W F (P ) |= Qi θ if and only if there is a correct answer substitution γ for Gi such that
θ is an instance of γ.
For a positive program, the well-founded semantics has a unique two-valued (minimal)
17

model and the generalized SLT-tree GTG0 returned by SLT P (P, G0, R, ∅, ∅) contains only
success and failure leaves. So the following result is immediate to Corollary 3.6.
Corollary 3.7 Let P be a positive program with the bounded-term-size property, G0 a top
goal, and GTG0 the generalized SLT-tree returned by SLT P (P, G0, R, ∅, ∅). For any goal
Gi =← Qi at some node Ni in GTG0 , if all branches starting at Ni end with a failure leaf
then W F (P ) |= ¬∃(Qi ).
Apparently Corollary 3.7 does not hold with general logic programs because their generalized SLT-trees may contain temporarily undefined leaves. For instance, although N10
labeled by ← r in Figure 1 ends only with a failure leaf, r is not false in W F (P1 ) because
it has another sub-derivation in GT←p(X) , N6 → N7 → N12 , that ends with a temporarily
undefined leaf. However, it turns out that the ground atom w in Figure 1 is false in W F (P1 )
because all its sub-derivations (i.e., N16 and N4 → N14 → N17 ) end with a failure leaf. This
observation is supported by the following theorem.
Theorem 3.8 Let P be a program with the bounded-term-size property and GTG0 the generalized SLT-tree returned by SLT P (P, G0, R, ∅, ∅). Let T Bt consist of all tabled positive
answers in GTG0
1. For any selected positive literal A in GTG0 , Aθ ∈ MP (∅) if and only if there is a correct
answer substitution for A in GTG0 that is more general than θ if and only if there is
an A′ ∈ T Bt with Aθ as an instance. In particular, when A is ground, A ∈ MP (∅) if
and only if A ∈ T Bt .
2. Let A be a selected ground positive literal in GTG0 . Let S be the set of selected subgoals at
the leaf nodes of all sub-derivations for A. A ∈ NP (∅) if and only if all sub-derivations
for A and S end with a failure leaf.
Proof: 1. Note that clauses with negative literals in their bodies do not contribute to
deriving positive answers in MP (∅) (see Definition 2.2). This is true in SLT P (P, G0, R, ∅, ∅)
as well because a selected subgoal ¬B either fails (when B succeeds) or is temporarily
undefined (otherwise). Let P + be a positive program obtained from P by removing all
clauses with negative literals in their bodies. Then MP (∅) = MP + (∅) and all tabled positive
answers in GTG0 are derived from P + ∪ {G0 }. Since MP + (∅) is the positive part of W F (P + ),
we have
Aθ ∈ MP (∅)⇐⇒ Aθ ∈ MP + (∅)
⇐⇒ W F (P + ) |= Aθ
⇐⇒ (By Corollary 3.6) there is an answer substitution for A in GTG0
that is more general than θ
⇐⇒ there is an A′ ∈ T Bt with Aθ as an instance.
18

When A is ground,
A ∈ MP (∅)⇐⇒ there is an answer substitution for A in GTG0
⇐⇒ (By Definition 3.5) there is a successful sub-derivation for A in GTG0
⇐⇒ A ∈ T Bt .
2. (⇐=) By point 1 above A 6∈ MP (∅). Suppose, on the contrary, that A ∈ OP (∅). Then
by Definition 2.5 there exists a clause C in P of the form
A′ ← B1 , ..., Bm , ¬D1 , ..., ¬Dn
such that one of its Herbrand instantiated clauses is of the form
A ← (B1 , ..., Bm , ¬D1 , ..., ¬Dn )θ
where no Di θ is in MP (∅) and each Bi θ is either in MP (∅) or in OP (∅). That is, A can be
derived through a backward chain of the form
A ⇒S1 B1 θ, ..., Bm θ, ¬D1 θ, ..., ¬Dn θ ⇒S2 E1 , ..., ¬Fk ⇒S3 ... ⇒St ✷
where each step is performed by either resolving a ground positive literal like Bi θ with an
answer in MP (∅) (if Bi θ ∈ MP (∅)) or with a Herbrand instantiated clause of P (otherwise),
or removing a negative literal like ¬Di θ where Di θ 6∈ MP (∅).
Based on point 1 above, it is easy to construct a sub-derivation for A, using clauses in
P and tabled answers in T Bt , that corresponds to the above backward chain. First we have
← A ⇒C,θ0 ← B1 θ0 , ..., Bm θ0 , ¬D1 θ0 , ..., ¬Dn θ0
where θ0 is the most general unifier of A and A′ . For each Bi θ0 , if Bi θ is resolved with a
Herbrand instantiated clause of P (resp. with an answer in MP (∅)) then there is a clause in
P (resp. a tabled positive answer in T Bt ) to resolve with Bi θ0 . For each ¬Di θ0 , if θ0 = θ
then ¬Di θ0 is treated as u∗ . As a result, we will generate a sub-derivation for A of the form
← A ⇒C,θ0 ... ⇒Ci−1 ,θi−1 ← L1 , L2 , ..., Lk ⇒Ci ,θi ... ⇒Cl ,θl ✷u∗
If no looping clause is used along the above sub-derivation for A, this sub-derivation
must be in GTG0 . Otherwise, without loss of generality assume the above sub-derivation is
of the form
← A ⇒C,θ0 ... ← L1 , L2 , ..., Lk ⇒Ci ,θi ... ← L′1 , F1 , ..., Fj , (L2 , ..., Lk )γ ⇒Ci ,θi′ ... ⇒Cl ,θl ✷u∗
where L1 is an ancestor variant subgoal of L′1 and L′1 is selected to resolve with the looping
clause Ci . It is easily seen that this sub-derivation can be shortened by removing the subderivation between L1 and L′1 because if L′1 , F1 , ..., Fj , (L2 , ..., Lk )γ can be reduced to ✷u∗ , so
can L1 , L2 , ..., Lk . Obviously, the shortened sub-derivation (or its variant form) will appear
in GTG0 . This contradicts that all sub-derivations of A and S in GTG0 end with a failure
leaf.
(=⇒) Assume A ∈ NP (∅) but, on the contrary, that there is a sub-derivation for A in
GTG0 that ends with a temporarily undefined leaf. Let the sub-derivation be of the form
← A ⇒C,θ0 ... ⇒Ci−1 ,θi−1 ← L1 , L2 , ..., Lk ⇒Ci ,θi ... ⇒Cl ,θl ✷u∗
where each derivation step is done by either resolving a selected positive literal with a clause
in P or with a tabled positive answer in T Bt , or treating a selected negative ground literal
19

¬F as u∗ where F 6∈ T Bt . Since by point 1 of this theorem MP (∅) consists of all (Herbrand)
ground instances of tabled positive answer in T Bt , the above sub-derivation must have a
Herbrand instantiated ground instance of the form
A ⇒S1 ... ⇒Sj E1 , ..., Em , ¬F1 , ..., ¬Fn ⇒Sj+1 ... ⇒St ✷
where each step is performed by either resolving a positive ground literal with a Herbrand
instantiated clause of P or with an answer in MP (∅), or removing a negative ground literal
¬F where F 6∈ MP (∅). However, by Definition 2.5 the above backward chain implies that A
is in OP (∅), contradicting A ∈ NP (∅).
Now assume that A ∈ NP (∅) and all sub-derivations for A end with a failure leaf, but, on
the contrary, that there is a sub-derivation for B ∈ S in GTG0 that ends with a temporarily
undefined leaf. Then B must be an ancestor subgoal of B. That is, there must be two
sub-derivations for B in GTG0 of the form
← B ⇒ ... ← A, ... ⇒ ... ⇒ ✷f ← B, ...
← B ⇒ ... ⇒ ✷u∗
The first sub-derivation suggests that the answers of A depend on B. By the first part of
the argument for (=⇒), the second sub-derivation implies B 6∈ NP (∅). Combining the two
leads to A 6∈ NP (∅), which contradicts the assumption A ∈ NP (∅). ✷
Theorem 3.8 is useful, by which the truth value of all selected ground negative literals
can be determined in an iterative way. For any selected ground negative literal ¬A, if all
sub-derivations of A and S (defined in Theorem 3.8) in GTG0 end with a failure leaf, A is
called a tabled negative answer. All tabled negative answers will be collected in T Bf .
We are now in a position to define SLT-resolution for general logic programs.
Definition 3.7 (SLT-resolution) Let P be a program, G0 a top goal and R a computation
rule. SLT-resolution proves G0 by calling the function SLT (P, G0, R, ∅, ∅), which is defined
as follows:
function SLT (P, G0 , R, T Bt , T Bf ) return a generalized SLT-tree GTG0
begin
GTG0 = SLT P (P, G0, R, T Bt , T Bf );
NEWt collects all tabled positive answers in GTG0 but not in T Bt ;
NEWf collects all tabled negative answers in GTG0 but not in T Bf ;
if NEWf = ∅ then return GTG0
else return SLT (P ∪ NEWt , G0 , R, T Bt ∪ NEWt , T Bf ∪ NEWf )
end
Definition 3.8 Let G0 =← Q0 be a top goal and TG0 be the top SLT-tree in GTG0 which
is returned by SLT (P, G0, R, ∅, ∅). G0 is true in P with an answer Q0 θ if there is a correct
answer substitution for G0 in TG0 that is more general than θ; false in P if all branches of TG0
end with a failure leaf; undefined in P if neither G0 is false nor TG0 has successful branches.
20

Example 3.2 (Cont. of Example 3.1) To evaluate G0 =← p(X), we call SLT (P1 , G0 , R, ∅, ∅).
This immediately invokes SLT P (P1, G0 , R, ∅, ∅), which generates the generalized SLT-tree
GT←p(X) for (P1 ∪ {← p(X)}, ∅) as shown in Figure 1. The tabled positive answers in
GT←p(X) are then collected in NEWt0 , i.e. NEWt0 = {p(a), q(a)}. So P11 = P1 ∪ NEWt0 .
(Note that the bodyless program clause Cp2 can be ignored in P11 since it has become a
tabled answer. See Section 5.3 for such kind of optimizations). The generalized SLT-tree
1
GT←p(X)
for (P11 ∪ {← p(X)}, ∅) is then generated, which is like GT←p(X) except that N2
gets a new child node N2′ − a success leaf, by unifying q(X) with the tabled positive answer
q(a) in P11 (see Figure 3). Clearly, the addition of this success leaf does not yield any new
1
tabled positive answers, i.e. NEWt1 = ∅. Therefore SLT P (P1, G0 , R, ∅, ∅) returns GT←p(X)
.
N0 : p(X)

❍ Cp1
❍
❥
❍

p(a)

✟
✟
✙
✟

✷t
N1 :

N2 : q(X)

q(a) ✘✘

❍❍Cq3
✘ Cq ✙
✘
✾
✟✟
❥
❍
1 ✟ Cq2 ❄
✷t
N4 : w

N2′ : N3 : ¬r
..
..
..

✙
N6 : r
Cr1
❄

✙

❍

❄

❍ p(a)
❍
❥
❍

✷u∗ N14 : ¬w, v
N13 : u∗ . . . . .
❍
.
✙

✷f
N16 : w

N7 : ¬s

..
..
..

N5 : p(X)

Cw1
❄

✷t
N15 :

❍
❥
❍

✷f
N17 : v, u∗

❍
❥
❍
✷u∗
N12 : u∗

N8 : s
Cs1
❄

N9 : ¬r

..
..
..

✙
✷f
N10 : r

❍
❍
❥
❍
✷u∗
N11 : u∗

1
Figure 3: The generalized SLT-tree GT←p(X)
for (P11 ∪ {← p(X)}, ∅).
1
It is easily seen that GT←p(X)
contains one new tabled negative answer w; i.e. NEWf1 =
1
{w} (note that ¬w is a selected literal at N14 and all sub-derivations for w in GT←p(X)
end
1
0
1
1
1
1
with a failure leaf). Let T Bt = NEWt ∪ NEWt and T Bf = NEWf . Since NEWf 6= ∅,
SLT (P1 ∪T Bt1 , G0 , R, T Bt1 , T Bf1 ) is recursively called, which invokes SLT P (P1 ∪T Bt1 , G0 , R,
2
T Bt1 , T Bf1 ). This builds a generalized SLT-tree GT←p(X)
for (P12 ∪ {← p(X)}, T Bf1 ) where
2
P12 = P1 ∪ T Bt1 (see Figure 4). Obviously, GT←p(X)
contains neither new tabled positive
2
answers nor new tabled negative answers. Therefore, SLT-resolution stops with GT←p(X)
returned. By Definition 3.8, G0 is true with an answer p(a).

4

Soundness and Completeness of SLT-resolution

In this section we establish the termination, soundness and completeness of SLT-resolution.

21

N0 : p(X)

❍ Cp1
❍
❥
❍

p(a)

✟
✟
✙
✟

✷t
N1 :

N2 : q(X)

q(a) ✘✘

❍❍Cq3
✘ Cq ✙
✘
✾
✟✟
❥
❍
1 ✟ Cq2 ❄
✷t

N2′ : N3 .: ¬r
.
..
..

✙
N6 : r
Cr1
❄

N4 : w

❄

❍

✙

❍ p(a)
❍
❥
❍

✷u∗ N14 : ¬w, v
N13 : u∗
❍

✷t
N15 :

❍
❥¬w
❍

✷f
N17 : v, u∗

N7 .: ¬s

.
..
..

N5 : p(X)

Cw1
❄

❍
❥
❍
✷u∗
N12 : u∗

N8 : s
Cs1
❄

N9 : . ¬r
..
✙

✷f
N10 : r

.
..

❍
❍
❥
❍
✷u∗
N11 : u∗

2
Figure 4: The generalized SLT-tree GT←p(X)
for (P12 ∪ {← p(X)}, T Bf1 ).

Theorem 4.1 For programs with the bounded-term-size property SLT-resolution terminates
in finite time.
Proof: Let P be a program with the bounded-term-size property. Since P has only a finite
number of clauses, we have only a finite number, say N, of ground subgoals in all generalized
SLT-trees GTGi 0 s. Before SLT-resolution stops, in each new recursion via SLT () at least one
new tabled negative answer will be derived. Therefore, there are at most N recursions
in SLT-resolution. By Theorem 3.3, each recursion (i.e. the execution of SLT P ()) will
terminate in finite time, so we conclude the proof. ✷
By Theorem 4.1, for programs with the bounded-term-size property, by calling SLT (P,
G0 , R, ∅, ∅) SLT-resolution generates a finite sequence of generalized SLT-trees:
GTG1 0 = SLT P (P, G0, R, ∅, ∅),
GTG2 0 = SLT P (P 1, G0 , R, T Bt1, T Bf1 ),
..
.

(3)

GTGk+1
= SLT P (P k , G0 , R, T Btk , T Bfk ),
0
where for each 1 ≤ i ≤ k, P i = P ∪ T Bti , and T Bti and T Bfi respectively consist of all tabled
positive and negative answers in all GTGj 0 s (j ≤ i). GTGk+1
will be returned since it contains
0
no new tabled answers (see Definition 3.7).
To simplify our presentation, in the following lemmas/corollaries/theorems, we assume
that P is a program with the bounded-term-size property, G0 is a top goal, GTG0 = GTGk+1
0
is as defined in (3), and TG0 is the top SLT-tree in GTG0 .

22

Lemma 4.2 Let GTGi 0 (i ≥ 1) be as defined in (3). For any selected ground subgoal A in
GTGi+1
, if A is in T Bfi then all sub-derivations for A in GTGi+1
will end with a failure leaf.
0
0
Proof: A ∈ T Bfi indicates that if A is a selected ground subgoal in GTGi 0 , all its subderivations end with a failure leaf. This implies that the truth value of A does not depend
on any selected negative subgoals whose truth values are temporarily undefined in GTGi 0 .
is derived from GTGi 0 simply by treating some selected negative subgoals ¬B
Since GTGi+1
0
whose truth values are temporarily undefined in GTGi 0 as true by assuming B is false, such
process obviously will not affect the truth value of A. Therefore, all sub-derivations for A in
GTGi+1
will end with a failure leaf. ✷
0
Lemma 4.3
1. For any selected positive literal A in GTG0 , there is a correct answer substitution γ for
A in GTG0 if and only if Aγ ∈ T Btk (up to variable renaming).
2. For any selected positive literal A at any node Ni in TG0 , there is a correct answer
substitution γ for A in GTG0 if and only if there is a correct answer substitution γ for
A at node Ni in TG0 (up to variable renaming).
Proof: Point 1 is straightforward by the fact that GTG0 contains no new tabled positive
answers. By point 1, all correct answer substitutions for A in GTG0 are in T Btk . Hence point
2 follows immediately from the fact that the selected literal A at node Ni in TG0 will use all
tabled answers in T Btk that unify with A. ✷
Lemma 4.4 For any selected positive literal A in GTG0 , Aθ ∈ MP k (¬.T Bfk ) if and only if
there is a correct answer substitution for A in GTG0 that is more general than θ, and for any
selected ground positive literal A in GTG0 , A ∈ NP k (¬.T Bfk ) if and only if all sub-derivations
for A and S (defined in Theorem 3.8) end with a failure leaf.
Proof: Let GTG1 0 = SLT P (P, G0, R, ∅, ∅) and T Bt1 and T Bf1 consist of all tabled positive
and negative answers in GTG1 0 , respectively. By Theorem 3.8, for any selected positive literal
A in GTG1 0 , Aθ ∈ MP (∅) if and only if there is a correct answer substitution for A in GTG1 0
that is more general than θ, and that for any selected ground negative literal ¬A in GTG1 0 ,
A ∈ NP (∅) if and only if all sub-derivations for A in GTG1 0 end with a failure leaf. Let
P 1 = P ∪ T Bt1 . Then P 1 is equivalent to P under the well-founded semantics.
Let GTG2 0 = SLT P (P 1, G0 , R, T Bt1 , T Bf1 ). Observe that SLT P (P 1, G0 , R, T Bt1 , T Bf1 )
works in the same way as SLT P (P 1, G0 , R, ∅, ∅) except whenever a negative subgoal ¬A
with A ∈ T Bf1 is selected, it will directly be treated as true instead of trying to prove A by
building a child SLT-tree T←A for ← A. When a positive subgoal A ∈ T Bf1 is selected, all subderivations for A will still be generated. However, By Lemma 4.2 all these sub-derivations will
23

end with a failure leaf, which implies that A is false. Therefore SLT P (P 1, G0 , R, T Bt1 , T Bf1 )
can be viewed as SLT P (P 1, G0 , R, ∅, ∅) with the exception that all selected ground subgoals in T Bf1 are treated as false instead of being temporarily undefined. This means that
SLT P (P 1, G0 , R, T Bt1 , T Bf1 ) has the same relationship to MP 1 (¬.T Bf1 ) and NP 1 (¬.T Bf1 ) as
SLT P (P 1, G0 , R, ∅, ∅) to MP 1 (∅) and NP 1 (∅). That is, by Theorem 3.8 for any selected positive literal A in GTG2 0 , Aθ ∈ MP 1 (¬.T Bf1 ) if and only if there is a correct answer substitution
for A in GTG2 0 that is more general than θ, and for any selected ground literal A in GTG2 0 ,
A ∈ NP 1 (¬.T Bf1 ) if and only if all sub-derivations for A and S in GTG2 0 end with a failure
leaf.
Continuing the above arguments, we will reach the same conclusion for any GTGi+1
=
0
i
i
i
SLT P (P , G0 , R, T Bt , T Bf ) with i ≥ 1. ✷
In the above proof we have T Bf1 ⊆ NP (∅), so that ¬.T Bf1 ⊆ W F (P ). Meanwhile, for
each A ∈ T Bt1 we have MP (∅) |= ∀(A), so that W F (P ) |= ∀(A). Therefore, P 1 = P ∪ T Bt1
is equivalent to P under the well-founded semantics, and by Lemma 2.2 MP 1 (¬.T Bf1 ) ⊆
W F (P ) and ¬.NP 1 (¬.T Bf1 ) ⊆ W F (P ). For the same reason we have T Bf2 ⊆ NP 1 (¬.T Bf1 ),
so that ¬.T Bf2 ⊆ W F (P ); and for each A ∈ T Bt2 we have MP 1 (¬.T Bf1 ) |= ∀(A), so that
W F (P ) |= ∀(A). This leads to P 2 = P ∪ T Bt2 being equivalent to P under the well-founded
semantics, MP 2 (¬.T Bf2 ) ⊆ W F (P ) and ¬.NP 2 (¬.T Bf2 ) ⊆ W F (P ). Repeating this process
leads to the following result.
Corollary 4.5 For any i ≥ 1, if A ∈ T Bfi then W F (P ) |= ¬A, and if A ∈ T Bti then
W F (P ) |= ∀(A).
Lemma 4.6
1. Let A be a selected positive literal in GTG0 . For any (Herbrand) ground instance Aθ of
A, W F (P ) |= Aθ if and only if Aθ ∈ MP k (¬.T Bfk ).
2. For any selected ground negative literal ¬A in GTG0 , W F (P ) |= ¬A if and only if
A ∈ T Bfk .
Proof: 1. (⇐=) Assume Aθ ∈ MP k (¬.T Bfk ). By Lemma 4.4 there is a correct answer
substitution for A in GTG0 that is more general than θ. Since T Btk consists of all tabled
positive answers in all GTGi 0 s (i ≥ 1), there is an Aγ ∈ T Btk with γ more general than θ. By
Corollary 4.5 W F (P ) |= ∀(Aγ), so that W F (P ) |= Aθ.
(=⇒) Assume W F (P ) |= Aθ. Since P k is equivalent to P under the well-founded semantics, W F (P k ) |= Aθ. Assume, on the contrary, Aθ 6∈ MP k (¬.T Bfk ). Since ¬.NP k (¬.T Bfk )
⊆ W F (P k ), Aθ is in OP k (¬.T Bfk ). So there exists a ground backward chain of the form
Aθ ⇒S1 ... ⇒Si B1 , ..., Bm , ¬D1 , ..., ¬Dn ⇒Si+1 ... ⇒St ✷
24

(4)

where each step is performed by either resolving a positive literal like Bj with an answer
in MP k (¬.T Bfk ) (when Bj ∈ MP k (¬.T Bfk )) or with a Herbrand instantiated clause of P
(otherwise), or removing a negative literal like ¬Dj where Dj 6∈ MP k (¬.T Bfk ). Observe that
for each negative literal ¬D occurring in the chain, either D ∈ T Bfk or D ∈ OP k (¬.T Bfk ) or
D ∈ NP k (¬.T Bfk ). However, since Aθ is true in W F (P k ), D must be false in W F (P k ). If D
is in T Bfk , it has already been treated to be false; otherwise, by Definition 2.3 ¬D cannot be
derived unless we assume some atoms in NP k (¬.T Bfk ) − T Bfk to be false. This implies that
for each negative literal ¬D occurring in the above chain with D 6∈ T Bfk , the proof of D will
be recursively reduced to the proof of some literals in NP k (¬.T Bfk ) − T Bfk .
By using similar arguments of Theorem 3.8, we can have a sub-derivation SDA for
A in GTG0 , which corresponds to the backward chain (4), that ends with a temporarily
undefined leaf. In SDA , each selected ground negative literal ¬D is true if D ∈ T Bfk ;
temporarily undefined, otherwise (note D 6∈ MP k (¬.T Bfk )). Since the sub-derivation ends
with a temporarily undefined leaf, it has at least one selected ground negative literal ¬D
with D 6∈ T Bfk . Let
S = {D|D 6∈ T Bfk and ¬D is a selected ground negative literal in SDA }.
Then by Lemma 2.3 each D ∈ S is either in NP k (¬.T Bfk ) − T Bfk or in OP k (¬.T Bfk ). We
consider two cases.
Case 1. There exists a D ∈ S with D ∈ NP k (¬.T Bfk ) − T Bfk . By Lemma 4.4 all subderivations for D in GTG0 end with a failure leaf. Since D is not in T Bfk , it is a new tabled
negative answer in GTG0 , which contradicts that GTG0 has no new tabled negative answers.
Case 2. Every D ∈ S is in OP k (¬.T Bfk ). Since the backward chain (4) is an instance
of the sub-derivation SDA , all Ds in S must be false in W F (P k ). However, as discussed
above no ¬D can be derived unless we assume some atoms in NP k (¬.T Bfk ) −T Bfk to be false.
That is, the proof of each D ∈ S can be recursively reduced to the proof of some literals in
NP k (¬.T Bfk ) − T Bfk . So GTG0 must have a subpath of the form
...¬D · · · ⊲ D ⇒ ... ⇒
...¬E1 · · · ⊲ E1 ⇒ ... ⇒
..
.
...¬Et · · · ⊲ Et
where Et ∈ NP k (¬.T Bfk ) − T Bfk . For the same reason as in the first case, Et should be a
new tabled negative answer in GTG0 , which leads to a contradiction.
2. (⇐=) Immediate from Corollary 4.5.
(=⇒) Assume W F (P ) |= ¬A but on the contrary A 6∈ T Bfk . By point 1 of this lemma,
A 6∈ MP k (¬.T Bfk ). If A ∈ NP k (¬.T Bfk ) then by Lemma 4.4 all sub-derivations for A in
GTG0 will end with a failure leaf. Since A is not in T Bfk , it is a new tabled negative answer,
contradicting that GTG0 has no new tabled negative answers. So A ∈ OP k (¬.T Bfk ).
25

Similar to the arguments for point 1 of this lemma, the proof of A can be recursively
reduced to the proof of some literals in NP k (¬.T Bfk ) − T Bfk , which will lead to new tabled
negative answers in GTG0 , a contradiction. ✷
Lemma 4.7 Let G0 ← A be a top goal (with A an atom). W F (P ) |= ¬∃(A) if and only if
all branches of TG0 end with a failure leaf.
Proof: (⇐=) Assume all branches of TG0 end with a failure leaf. Let Aθ be a ground instance
of A. By Lemmas 4.3 (point 2) and 4.4, Aθ 6∈ MP k (¬.T Bfk ), so by Lemma 4.6 W F (P ) 6|= Aθ.
Assume, on the contrary, W F (P ) 6|= ¬Aθ. By Corollary 4.5, Aθ 6∈ NP k (¬.T Bfk ) and thus
Aθ ∈ OP k (¬.T Bfk ). Then there exists a ground backward chain of the form
Aθ ⇒S1 ... ⇒Si B1 , ..., Bm , ¬D1 , ..., ¬Dn ⇒Si+1 ... ⇒St ✷

(5)

where each step is performed by either resolving a positive literal like Bj with an answer
in MP k (¬.T Bfk ) (when Bj ∈ MP k (¬.T Bfk )) or with a Herbrand instantiated clause of P
(otherwise), or removing a negative literal like ¬Dj where Dj 6∈ MP k (¬.T Bfk ). Observe that
for each negative literal ¬D occurring in the chain, either D ∈ T Bfk or D ∈ OP k (¬.T Bfk )
or D ∈ NP k (¬.T Bfk ). However, since Aθ is neither true nor false in W F (P ), there exists at
least one D ∈ OP k (¬.T Bfk ).
By using similar arguments of Theorem 3.8, TG0 must have a branch, which corresponds
to the backward chain (5), that ends with a temporarily undefined leaf. This contradicts
the assumption that all branches of TG0 end with a failure leaf. Therefore, for any ground
instance Aθ of A W F (P ) |= ¬Aθ. That is, W F (P ) |= ¬∃(A).
(=⇒) Assume W F (P ) |= ¬∃(A). By Lemmas 4.6 and 4.4, there is no sub-derivation for
A that ends with a success leaf in GTG0 .
Now assume, on the contrary, that TG0 has a branch BR that ends with a temporarily
undefined leaf. Then BR has at least one ground instance corresponding to the ground
backward chain like (5). Since Aθ is false in W F (P ), there exists at least one ground
negative literal ¬D in the chain such that D is true in W F (P ). This means that there is a
selected ground negative literal ¬D in BR such that D is true in W F (P ). By Corollary 4.5
D 6∈ T Bfk , so by Definition 3.3 a child SLT-tree T←D must be built where D is a selected
positive literal. Since BR is a temporarily undefined branch, ¬D cannot fail, so T←D has
no successful branch (i.e. ¬D is treated as u∗ ; see point 4 of Definition 3.3). By Lemma
4.4 D 6∈ MP k (¬.T Bfk ) and by Lemma 4.6 W F (P ) 6|= D, which contradicts that D is true in
W F (P ). Therefore, all branches of TG0 must end with a failure leaf. ✷
Now we are ready to show the soundness and completeness of SLT-resolution.
Theorem 4.8 Let P̄ be the augmented version of P . Let G0 ← A be a top goal (with A
an atom) and θ a substitution for the variables of A. Assume neither A nor θ contains the
symbols p̄ or f¯ or c̄.
26

1. W F (P ) |= ∃(A) if and only if G0 is true in P with an instance of A;
2. W F (P ) |= ¬∃(A) if and only if G0 is false in P ;
3. W F (P ) 6|= ∃(A) and W F (P ) 6|= ¬∃(A) if and only if G0 is undefined in P ;
4. If G0 is true in P with an answer Aθ then W F (P ) |= ∀(Aθ);
5. If W F (P̄ ) |= ∀(Aθ) then G0 is true in P with an answer Aθ.
Proof:
1. Immediate from Lemmas 4.4 and 4.6.
2. Immediate from Lemma 4.7.
3. Immediate from points 1 and 2 of this theorem.
4. Assume G0 is true in P with an answer Aθ. Then there is a correct answer substitution γ in TG0 that is more general than θ. By Theorem 3.2 W F (P k ) |= ∀(Aγ) and
thus W F (P ) |= ∀(Aγ) since P k is equivalent to P w.r.t. the well-founded semantics.
Therefore W F (P ) |= ∀(Aθ).
5. Note that P̄ = P ∪ {p̄(f¯(c̄))}. Let TG′ 0 be the top SLT-tree in GTG′ 0 that is returned
by SLT (P̄ , G0 , R, ∅, ∅). Since none of the symbols p̄ or f¯ or c̄ appears in P ∪ {G0 },
TG′ 0 = TG0 and GTG′ 0 = GTG0 .
Let {X0 , ..., Xn } be the set of variables appearing in Aθ and α be the ground substitution {X0 /c̄, X1 /f¯(c̄), ..., Xn /f¯n (c̄)}. Then W F (P̄ ) |= Aθα and by Lemmas 4.6, 4.4 and
4.3 there is a correct answer substitution γ for G0 in TG′ 0 that is more general than θα.
That is, there exists a substitution β such that γβ = θα. Since TG′ 0 = TG0 , γ contains
neither f¯ nor c̄. So the only occurrences of f¯ and c̄ in γβ are in β. Let β ′ be obtained
from β by replacing every occurrence of f¯i (c̄) by the variable Xi . Then γβ ′ = θ and
thus γ is more general than θ.
Since TG′ 0 = TG0 , there is a correct answer substitution γ for G0 in TG0 that is more
general than θ. Therefore, by Definition 3.8 G0 is true in P with an answer Aθ. ✷
Observe that in point 5 of Theorem 4.8 we used the augmented program P̄ to characterize part of the completeness of SLT-resolution. The concept of augmented programs was
introduced by Van Gelder, Ross and Schlipf [33], which is used to deal with the so called
universal query problem [17]. As indicated by Ross [22], we cannot substitute P for P̄ in
point 5 of Theorem 4.8. A very simple illustrating example is that let P = {p(a)} and
G0 =← p(X), we have W F (P ) |= ∀(p(X){X/X}) under Herbrand interpretations, but we
have no correct answer substitution for G0 in TG0 that is more general than {X/X}.
27

5

Optimizations of SLT-resolution

The objective of this paper is to develop an evaluation procedure for the well-founded semantics that is linear, free of infinite loops and with less redundant computations. Clearly,
SLT-resolution is linear and with no infinite loops. However, like SLDNF-trees, SLT-trees
defined in Definition 3.3 may contain a lot of duplicated sub-branches. SLT-resolution can
be considerably optimized by eliminating those redundant computations. In this section we
present three effective methods for the optimization of SLT-resolution.

5.1

Negation as the Finite Failure of Loop-Independent Nodes

From Definition 3.7 we see that SLT-resolution exhausts the answers of the top goal G0 by
recursively calling the function SLT P (). Obviously, the less the number of recursions is,
the more efficient SLT-resolution would be. In this subsection we identify a large class of
recursions that can easily be avoided. We start with an example.
Example 5.1 Consider the following program:
P2 : a ← ¬b.
b ← ¬c.
c ← ¬d.

Ca1
Cb1
Cc 1

Let G0 =← a be the top goal. Calling SLT (P2 , G0 , R, ∅, ∅) immediately invokes SLT P (P2, G0 ,
1
as shown in Figure 5 (a). Since
R, ∅, ∅), which builds the first generalized SLT-tree GT←a
1
1
there is no tabled positive answer in GT←a (T Bt = ∅), the first tabled negative answer d
is derived, which yields T Bf1 = {d}. Then SLT (P2 , G0 , R, ∅, T Bf1 ) is called, which invokes
2
as shown in FigSLT P (P2 , G0 , R, ∅, T Bf1 ) that builds the second generalized SLT-tree GT←a
2
ure 5 (b). GT←a has a new tabled positive answer c, so SLT P (P2 ∪ {c}, G0 , R, {c}, T Bf1 )
is executed, which produces no new tabled positive answers. The second tabled negative
2
answer b is then obtained from GT←a
. So far, T Bt2 = {c} and T Bf2 = {b, d}. Next,
SLT (P2 ∪T Bt2 , G0 , R, T Bt2 , T Bf2 ) is called, which invokes SLT P (P2 ∪T Bt2 , G0 , R, T Bt2 , T Bf2 )
3
that builds the third generalized SLT-tree GT←a
as shown in Figure 5 (c). We see a is true
3
in GT←a . As a result, to derive the first answer of a SLT () is called three times and SLT P ()
four times.
1
Carefully examining the generalized SLT-tree GT←a
in Figure 5, we notice that it contains no loops. That is, all nodes in it are loop-independent. Consider the selected positive
literal d at N6 . Since there is no sub-derivation for d starting at N6 that ends with a temporarily undefined leaf and the proof of d is independent of all its ancestor subgoals, the set
of sub-derivations for d will remain unchanged throughout the recursions of SLT (); i.e. it
i
will not change in all GT←a
s (i > 1) in which d is a selected positive literal. This means

28

N0 : a

N0 : a

Ca1

Ca1

❄

❄

N1 : . ¬b

N1 : . ¬b
..
✙

.
..

N2 : b
Cb1
❄

..
✙

❄

N2 : b

✷u∗
N9 : u∗

Cb1
❄

✷f
N. 3. .: ¬c

N3 .: ¬c

.
..
..

✙
N4 : c

..
✙

❄

✷u∗
N8 : u∗

..
✙

✷f
N6 : d

.

Ca1

❄

N1 : ¬b

2

❄
✷u∗
N7 : u∗

b ∈ T Bf
❄

✷t
N2 :
3
(c) GT←a

N4 : c

Cc1
❄

N5 : . ¬d

.
..

N0 : a

Cc1
❄

N5 : ¬d

1

d ∈ T Bf
❄

.
..

❄

✷t
N6 :

✷u∗
N7 : u∗
1
(a) GT←a

2
(b) GT←a

1
2
3
Figure 5: The generalized SLT-trees GT←a
, GT←a
and GT←a
.

that all answers of d can be determined only based on its sub-derivations starting at N6 in
1
GT←a
, which leads to the following result.
Theorem 5.1 Let GTG0 = GTGk+1
= SLT P (P k , G0 , R, T Btk , T Bfk ), which is returned by
0
SLT (P, G0, R, ∅, ∅). Let A be a selected positive literal at a loop-independent node Ni in
= SLT P (P j , G0 , R, T Btj , T Bfj ) (j ≤ k) in which all sub-derivations SDA for A startGTGj+1
0
ing at Ni end with a non-temporarily undefined leaf. Then θ is a correct answer substitution
for A in SDA if and only if Aθ is a tabled positive answer for A in T Btk ; and A is false in
P if and only if all branches of SDA end with a failure leaf.
Proof: Let T←A be the SLT-tree for (P ∪ {← A}, T Bfj ). Since Ni is loop-independent,
SDA = T←A . Furthermore, since no branches in T←A end with a temporarily undefined leaf,
no new sub-derivations for A will be generated via further recursions of SLT (). Therefore,
in view of the fact that T Btk consists of all tabled positive answers in all GTGl 0 s, θ is a correct
answer substitution for A in SDA if and only if Aθ is a tabled positive answer for A in T Btk .
And by Lemma 4.7, A is false in P if and only if all branches of SDA end with a failure leaf.
✷
Theorem 5.1 allows us to make the following enhancement of SLT-trees:
Optimization 1 In Definition 3.3 change (c) of point 4 to (d) and add before it
(c) If the root of T←A is loop-independent and all branches of T←A end with a failure leaf
then Ni has only one child that is labeled by the goal ← L1 , ..., Lj−1 , Lj+1, ..., Ln ;

29

Example 5.2 (Cont. of Example 5.1) By applying the optimized algorithm for constructing
1
SLT-trees, SLT-resolution will build the generalized SLT-tree GT←a
as shown in Figure 6.
Since N6 is loop-independent, by Theorem 5.1 d is false and thus ¬d is true, which leads to
c true and ¬c false. Likewise, since N2 is loop-independent, b is false, which leads to a true.
As a result, to derive the first answer of a SLT () is called ones and SLT P () ones, which
shows a great improvement in efficiency over the former version.
N0 : a
Ca1

❄

N1 : ¬b

..
..
..

✙

❄

N2 : b

✷t
N8 :

Cb1
❄

✷f
N3. .: ¬c
..
✙

..

N4 : c
Cc1
❄

N5 : ¬d

..
..
..

✙
✷f
N6 : d

❄

✷t
N7 :

1
Figure 6: The generalized SLT-tree GT←a
for (P2 ∪ {← a}, ∅).

It is easy to see that when the root of TG0 is loop-independent, TG0 is an SLDNFtree and thus SLT-resolution coincides with SLDNF-resolution. Due to this reason, we call
Optimization 1, which reduces recursions of SLT (), negation as the finite failure of loopindependent nodes.

5.2

Answer Completion

In this subsection we further optimize SLT-resolution by implementing the intuition that if
all answers of a positive literal A have been derived and stored in the table T Bti or T Bfi
after the generation of GTGi 0 , then all sub-derivations for A in GTGi+1
, which are generated
0
by applying program clauses (not tabled answers) to A, can be pruned because they produce
no new answers for A. Again we begin with an example.
Example 5.3 Let P3 be P2 of Example 5.1 plus the program clause Cp1 : p ← a, p. Let
G0 =← p. SLT-resolution (with Optimization 1) first builds the generalized SLT-tree GTG1 0
as shown in Figure 7 (a). Note that N1 − N7 are loop-independent nodes, and N0 and N9
are loop-dependent nodes. So T Bt1 = {c, a} and T Bf1 = {d, b}. Using these tabled answers
SLT-resolution then builds the second generalized SLT-tree GTG2 0 as shown in Figure 7 (b).
Since no new tabled positive answers are generated in GTG2 0 , p is judged to be false. Hence
30

T Bt2 = T Bt1 = {c, a} and T Bf2 = {d, b, p}. Since p is a new tabled negative answer, SLTresolution starts a new recursion SLT (P3 ∪T Bt2 , G0 , R, T Bt2, T Bf2 ), which will build the third
generalized SLT-tree GTG3 0 that is the same as GTG2 0 . Since GTG3 0 contains no new tabled
answers, the process stops.
N0 : p

N0 : p
Cp1
❄

N1 : a, p
Ca1

❄

N2 : ¬b, p

..
..
..

✙

N3 : b
Cb1
❄

N1 : a, p

✷f
N2 : p

❄

..

. . . . . . . . . . . ..
.. ❄
..
Ca1
..
..
N
:
¬b,
p
.. 3
..
.. ❄
b ∈ T Bf1 ..
.. ✷f
..
.. N4 : p
.
.. . . . . . . . . . . ...

✟
a ∈ T Bt1✟
✟ .
✙

✷f
N9 : p

✷f
N4 .: . ¬c
..
✙

Cp1
❄

. .0. .: .p. . . . . . . ..
.. . . . . . . . . . . . . N
..
..
Cp1
❄
..
..
N1 : a, p
..
..
1
✟
✟
.. a ∈ T Bt ✟
..
✙
Ca1
❄
..
..
✷f
N
:
¬b,
p
3
..
..
N2 : p
..
❄
b ∈ T Bf1 ..
..
..
✷f
..
.
N4 : p
.. . . . . . . . . . . . . . . . . . . . . . . . . ...

(b) GTG2 0

N5 : c

(c) GTG3 0

Cc1
❄

N6 : . ¬d
..
✙

✷f
N7 : d

.
..

❄

✷t
N8 :

(a) GTG1 0
Figure 7: The generalized SLT-trees GTG1 0 , GTG2 0 and GTG3 0 .
Examining GTG2 0 in Figure 7 we observe that since by Theorem 5.1 all answers of a have
already been stored in T Bt1 , the sub-derivation for a via the clause Ca1 (circumscribed by
the dotted box) is redundant and hence can be removed. Similarly, since the unique answer
of p has already been stored in T Bf2 , the circumscribed sub-derivations for p via the clause
Cp1 in GTG3 0 are redundant and thus can be removed. We now discuss how to realize such
type of optimization.
First, we associate with each selected positive literal A (or its variant) a completion flag
comp(A), defined by
comp(A) =





Y es if the answers of A are completed;
No otherwise.

We say the answers of A are completed if all its answers have been stored in some T Bti or T Bfi .
The determination of whether a selected positive literal A has got its complete answers is
based on Theorem 5.1. That is, for a selected positive literal A at node Nk , comp(A) = Y es
if Nk is loop-independent (assume Optimization 1 has already been applied). In addition,
for each tabled negative answer A in T Bfi , comp(A) should be Y es.
Then, before applying program clauses to a selected positive literal A as in point 3 of
Definition 3.3, we do the following:
31

Optimization 2 Check the flag comp(A). If it is Y es then apply to A no program clauses
but tabled answers.
Example 5.4 (Cont. of Example 5.3) Based on GTG1 0 in Figure 7, comp(a), comp(b),
comp(c) and comp(d) will be set to Y es since N1 , N3 , N5 and N7 are loop-independent.
Therefore, the circumscribed sub-derivation in GTG2 0 will not be generated by the optimized
SLT-resolution. Likewise, although N0 : p in GTG2 0 is loop-dependent, once p is added to
T Bf2 , comp(p) will be set to Y es. As a result, the circumscribed sub-derivations in GTG3 0
will never occur, so that GTG3 0 will consist only of a single failure leaf at its root.

5.3

Eliminating Duplicated Sub-Branches Based on a Fixed DepthFirst Control Strategy

Consider two selected positive literals A1 at node N1 and A2 at node N2 in GTGi 0 such that
A1 is a variant of A2 . Let {C1 , ..., Cm } be the set of program clauses in P whose heads
can unify with A1 . Then both A1 and A2 will use all the Cj s except for looping clauses.
This introduces obvious redundant sub-branches, starting at N1 and N2 respectively. In this
subsection we optimize SLT-resolution by eliminating this type of redundant computations.
We begin by making the following two simple and yet practical assumptions.
1. We assume that program clauses and tabled answers are stored separately, and that new
intermediate answers in SLT-trees are added into their tables once they are generated
(i.e. new tabled positive answers are collected during the construction of each GTGi 0 ).
All tabled answers can be used once they are added to tables. For instance, in Figure
6 the intermediate answer c is added to the table T Bt right after node N7 is generated.
Such an answer can then be used thereafter. Obviously, this assumption does not affect
the correctness of SLT-resolution.
2. We assume nodes in each GTGi 0 are generated one after another in an order specified by
a depth-first control strategy. A control strategy consists of a search rule, a computation
rule, and policies for selecting program clauses and tabled answers. A search rule is
a rule for selecting a node among all nodes in a generalized SLT-tree. A depth-first
search rule is a search rule that starting from the root node always selects the most
recently generated node. Depth-first rules are the most widely used search rules in
artificial intelligence and programming languages because they can be very efficiently
implemented using a simple stack-based memory structure. For this reason, in this
paper we choose depth-first control strategies, i.e. control strategies with a depth-first
search rule.
The intuitive idea behind the optimization is that after a clause Cj has been completely
used by A1 at N1 , it needs not be used by A2 at N2 . We describe how to achieve this.
32

Let CS be a depth-first control strategy and assume A1 at N1 is currently selected by
CS. Instead of generating all child nodes of N1 by simultaneously applying to A1 all program
clauses and tabled answers (as in point 3 of Definition 3.3), each time only one clause or
tabled answer, say Cj , is selected by CS to apply to A1 . This yields one child node, say Ns .
Then Ns will be immediately expanded in the same way (recursively) since it is the most
recently generated node. After the expansion of Ns has been finished, its parent node N1
is selected again by CS (since it is the most recently generated node among all unfinished
nodes) and expanded by applying to A1 another clause or tabled answer (selected by CS). If
no new clause or tabled answer is left for A1 , which means that all sub-branches starting at
N1 in GTGi 0 have been exhausted, the expansion of N1 is finished. The control is then back
to the parent node of N1 . This process is usually called backtracking. Continue this way
until we finish the expansion of the root node of GTGi 0 . Since GTGi 0 is finite (for programs
with the bounded-term-size property), CS is complete for SLT-resolution in the sense that
all nodes of GTGi 0 will be generated using this control strategy. This shows a significant
advantage over SLDNF-resolution, which is incomplete with a depth-first control strategy
because of possible infinite loops in SLDNF-trees [15]. Moreover, the above description
clearly demonstrates that SLT-resolution is linear for query evaluation.
In the above description, when backtracking to N1 from Ns , all sub-branches starting at
N1 via Cj in GTGi 0 must have been exhausted. In this case, we say Cj has been completely
used by A1 . For each program clause Cj whose head can unify with A1 , we associate with
A1 (or its variant) a flag comp used(A1 , Cj ), defined by
comp used(A1 , Cj ) =




Y es if Cj has been completely used by A1 (or its variant);
 No otherwise.

From the above description we see that given a fixed depth-first control strategy, program
clauses will be selected and applied in a fixed order. Therefore, by the time Cj is selected
for A2 at N2 , we check the flag comp used(A2, Cj ). If comp used(A2 , Cj ) = Y es then Cj
needs not be applied to A2 since similar sub-derivations have been completed before with
all intermediate answers along these sub-derivations already stored in tables for A2 to use
(under the above first assumption).
Observe that in addition to deriving new answers, the application of Cj to A1 may
change the property of loop dependency of N1 , which is important to Optimizations 1 and 2.
That is, if some sub-branch starting at N1 via Cj contains loop nodes then N1 will be loopdependent. If N1 is loop-dependent, neither Optimization 1 nor Optimization 2 is applicable,
so the answers of A1 can be completed only through the recursions of SLT-resolution. Since
A2 is a variant of A1 , N2 should have the same property as N1 . To achieve this, we associate
with A1 (or its variant) a flag loop depend(A1 ), defined by

33






Y es if A1 (or its variant) has been selected at some
loop depend(A1 ) =
loop-dependent node;



No otherwise.
Then at node N2 we check the flag. If loop depend(A2 ) = Y es then mark N2 as a loop node,
so that N2 becomes loop-dependent.
To sum up, SLT-trees can be generated using a fixed depth-first control strategy CS,
where the following mechanism is used for selecting program clauses (not tabled answers):
Optimization 3 Let A be the currently selected positive literal at node Nk . If loop depend(A)
= Y es, mark Nk as a loop node. A clause Cj is selected for A based on CS such that Cj is
not a looping clause of A and comp used(A, Cj ) = No.
Theorem 5.2 Optimization 3 is correct.
Proof: The exclusion of looping clauses has been justified in SLT-resolution before. Here we
justify the exclusion of program clauses that have been completely used. Let A1 at node N1
and A2 at node N2 be two variant subgoals in GTGi 0 and let Cj have been completely used
by A1 by the time Cj is selected for A2 . Since we use a fixed depth-first control strategy,
all sub-derivations for A1 via Cj must have been generated, independently of applying Cj to
A2 . This means that applying Cj to A2 will generate similar sub-derivations. Thus skipping
Cj at N2 will not lose any answers to A2 provided that A2 has access to the answers of A1
and that N2 has the same property of loop dependency as N1 . Clearly, that N2 has the same
property of loop dependency as N1 is guaranteed by using the flag loop depend(A1 ), and the
access of A2 to the answers of A1 is achieved by the first assumption above.
Observe that the application of the first assumption may lead to more sub-derivations
for A2 via Cj than those for A1 via Cj . These extra sub-branches are generated by using
some newly added tabled answers, S1 , during the construction of GTGi 0 , which were not yet
available during the generation of sub-derivations of A1 via Cj . If these extra sub-branches
would yield new tabled answers, S2 , the sub-derivations of A1 via Cj must have a loop. In
this case, however, the newly added tabled answers S1 will be applied to the generation of
sub-derivations of A1 via Cj in the next recursion of SLT-resolution, which produces similar
sub-branches with new tabled answers S2 . Since A2 is loop-dependent as A1 , it will be
generated in this recursion and use the answers S2 from A1 . ✷
The following two results show that redundant applications of program clauses to variant
subgoals are reduced by Optimization 3.
Theorem 5.3 Let A1 at node N1 be an ancestor variant subgoal of A2 at node N2 . The
program clauses used by the two subgoals are disjoint.
34

Proof: Let CS be a fixed depth-first control strategy and {C1 , ..., Cm } be the set of program
clauses whose heads can unify with A1 . Assume these clauses are selected by CS sequentially
from left to right. Since A1 at N1 is an ancestor variant of A2 at N2 , let Ci be the clause via
which the sub-branch starting at N1 leads to N2 . Obviously, Ci will not be used by A2 since
it is a looping clause of A2 .
By Optimization 3, for each 1 ≤ j < i by the time t when Ci was selected for A1 at N1 ,
Cj is either a looping clause of A1 or comp used(A1 , Cj ) = Y es. Since N2 was generated
after t, Cj is either a looping clause of A2 or comp used(A2, Cj ) = Y es. So Cj will not be
used by A2 at N2 .
Since CS adopts a depth-first search rule, by the time t1 when A1 tries to select the
next clause Ck (k > i) Ci must have been completely used by A1 (via backtracking). This
implies that all Cj s (i < j ≤ m) must have been completely used before t1 by A2 . Hence for
no i < j ≤ m Cj will be available to A1 . ✷
Theorem 5.4 Let A1 = p(.) and Cpj be a program clause whose head can unify with A1 .
Assume the number of tabled answers of A1 is bounded by N. Then Cpj is applied in GTGi 0
by O(N) variant subgoals of A1 .
Proof: Let {A1 , ..., Am } be the set of variant subgoals that are selected in GTGi 0 . The worst
case is like this: The application of Cpj to A1 yields the first tabled answer of A1 , but Cpj
has not yet been completely used after this. Next A2 is selected, which uses the first tabled
answer and then applies Cpj to produce the second tabled answer. Again Cpj has not yet been
completely used after this. Continue this way until AN +1 is selected, which uses all the N
tabled answers and then applies Cpj . This time it will fail to produce any new tabled answer
after exhausting all the remaining branches of AN +1 via Cpj . So Cpj has been completely
used by AN +1 and the flag comp used(AN +1 , Cpj ) is set to Y es. Therefore Cpj will never be
applied to any selected variant subgoals of A1 thereafter. ✷
Example 5.5 Consider the following program and let G0 =← p(X, 5) be the top goal.5
P3 : p(X, N) ← loop(N), p(Y, N), odd(Y ), X is Y + 1, X < N.
p(X, N) ← p(Y, N), even(Y ), X is Y + 1, X < N.
p(1, N).
loop(N).

Cp 1
Cp 2
Cp 3
Cl1

Here, odd(Y ) is true if Y is an odd number, and even(Y ) is true if Y is an even number.“
X is Y + 1” is a meta-predicate which computes Y + 1 and then assigns the result to X.
We assume using the Prolog control strategy: depth-first for node/goal selection + leftmost for subgoal selection + top-down for clause selection. Obviously, it is a depth-first
5

This program is suggested by B. Demon, K. Sagonas and N. F. Zhou.

35

control strategy. We also assume using the first-in-first-out policy for selecting answers in
tables. If both program clauses and tabled answers are available, tabled answers are used
first. Let CS represent the whole control strategy. Then SLT-resolution (enhanced with
Optimization 3) evaluates G0 step by step and generates a sequence of nodes N0 , N1 , N2 ,
and so on, as shown in Figures 8 and 9.
N0 : p(X, 5)

✏✏
✮✏
✏

PP p(1, 5)
PP
q

Cp1

N1 : loop(5), p(Y, 5), odd(Y ), X is Y + 1, X < 5

N10 : ✷t

C l1

❄

N2 : p(Y, 5), odd(Y ), X is Y + 1, X < 5

Cp2

✘
✘✘✘
✾

N3 : p(Y1 , 5), even(Y1 ), Y is Y1 + 1, Y < 5,

p(1, 5)
❄

N5 : odd(1), X is 1 + 1, X < 5

odd(Y ), X is Y + 1, X < 5
Cp3

Add p(1, 5) to T Bt1

❄

✷f
N4 : even(1), Y is 1 + 1, Y < 5,
odd(Y ), X is Y + 1, X < 5

❳❳
③

p(2, 5)

✷f
N9 : odd(2), X is 2 + 1, X < 5

❄
N6 : X is 1 + 1, X < 5
X=2
❄

N7 : 2 < 5
Add p(2, 5) to T Bt1

❄
N8 : ✷t

Figure 8: GTG1 0 .
Since P3 is a positive program, SLT (P3 , G0 , CS, ∅, ∅) = SLT P (P3 , G0 , CS, ∅, ∅). The
first generalized SLT-tree GTG1 0 is shown in Figure 8. We explain a few main points. At
N3 the (non-looping) program clause Cp3 is applied to p(Y1 , 5), which yields the first tabled
answer p(1, 5). p(1, 5) is immediately added to the table T Bt1 . After the failure of N4 , we
backtrack to N3 and then N2 . By this time Cp3 has been completely used by p(Y1, 5) at N3 ,
so we set comp used(p(Y1, 5), Cp3 ) = Y es. Due to this Cp3 is skipped at N2 . Applying the
first tabled answer p(1, 5) to p(Y, 5) at N2 generates N5 . At N8 the second tabled answer
p(2, 5) is produced, which yields the first answer to G0 . p(2, 5) is then applied to p(Y, 5) at
N2 , leading to N9 . When we backtrack to N0 from N9 , Cp2 has been completely used by
p(Y, 5) at N2 . So both Cp2 and Cp3 are ignored at N0 . The tabled answer p(1, 5) is then
applied to p(X, 5) at N0 , yielding the second answer p(1, 5) to G0 at N10 . Note that the
tabled answer p(2, 5) was obtained from a correct answer substitution for p(X, 5) at N0 , so
it was used by p(X, 5) while it was generated. As a result, GTG1 0 is completed with the table
T Bt1 = {p(1, 5), p(2, 5)}.
We then do the first recursion of SLT-resolution by calling SLT P (P3 ∪T Bt1 , G0 , CS, T Bt1 , ∅),
which builds the second generalized SLT-tree GTG2 0 as shown in Figure 9. From GTG2 0 we get
two new tabled answers p(3, 5) and p(4, 5). That is, T Bt2 = {p(1, 5), p(2, 5), p(3, 5), p(4, 5)}.
The second recursion of SLT-resolution is done by calling SLT P (P3∪T Bt2 , G0 , CS, T Bt2 , ∅),
which produces no new tabled answers. Therefore SLT-resolution stops here.

36

N0 : p(X, 5)
p(1, 5)

p(2, 5)

❄

N1 : ✷t

Cp1

❄

N2 : ✷t

p(3, 5)
❄

❄

N3 : loop(5), p(Y, 5), odd(Y ), X is Y + 1, X < 5 N29 : ✷t
C l1
❄

N4 : p(Y, 5), odd(Y ), X is Y + 1, X < 5
p(1, 5)

p(2, 5)

❄

N5 : odd(1),
X is 1 + 1, X < 5

Cp2

✷❄
f
N9 : odd(2), ...

❄
✷❄
f
N24 : odd(3),
N28 : odd(4), ...
X is 3 + 1, X < 5

odd(Y ), X is Y + 1, X < 5

❄
N6 : X is 1 + 1, X < 5

❄
N25 : X is 3 + 1, X < 5

X=2

X=4
❄

❄

N7 : 2 < 5

N26 : 4 < 5

❄

❄

N8 : ✷t
p(1, 5)
❄

N11

p(4, 5)

p(3, 5)

❄

N10 : p(Y1 , 5), even(Y1 ),
Y is Y1 + 1, Y < 5,

N27 : ✷t
p(2, 5)

p(3, 5)
❄

✷f
❄
: even(1), ... N12 : even(2),
Y is 2 + 1, Y < 5,

N19

p(4, 5)

✷f
: even(3), ...

N20 : even(4),
Y is 4 + 1, Y < 5,

N23

odd(Y ), X is Y + 1, X < 5

odd(Y ), X is Y + 1, X < 5

❄

❄
N21 : Y is 4 + 1, Y < 5,
odd(Y ), X is Y + 1, X < 5

N13 : Y is 2 + 1, Y < 5,
odd(Y ), X is Y + 1, X < 5
Y
❄

Cp3
❄

❄

=3

❄

✷f
N22 : 5 < 5, ...

N14 : 3 < 5, odd(3), X is 3 + 1, X < 5
2

Add p(3, 5) to T Bt
❄

N15 : odd(3), X is 3 + 1, X < 5

❄
N16 : X is 3 + 1, X < 5
X=4
❄

N17 : 4 < 5
Add p(4, 5) to T Bt2

❄
N18 : ✷t

Figure 9: GTG2 0 .

37

✷f
: even(1), ...

Remark 5.1 Consider node N10 in GTG2 0 (Figure 9). For each tabled answer p(E, N) with E
an even number, apply it to p(Y1 , N) will always produce two new tabled answers p(E +1, N)
and p(E + 2, N). Since these new answers will be fed back immediately to N10 for p(Y1 , N)
to use, all the remaining answers of G0 will be produced at N10 . This means that for any N
evaluating p(X, N) requires doing at most two recursions of SLT-resolution.
It is easy to combine Optimizations 1, 2 and 3 with Definition 3.3, which leads to an
algorithm for generating optimized SLT-trees based on a fixed depth-first control strategy, as
described in appendix A. This algorithm is useful for the implementation of SLT-resolution.

5.4

Computational Complexity of SLT-Resolution

Theorem 4.1 shows that SLT-resolution terminates in finite time for any programs with the
bounded-term-size property. In the above subsections we present three effective optimizations for reducing redundant computations. In this subsection we prove the computational
complexity of (the optimized) SLT-resolution.
SLT-resolution evaluates queries by building some generalized SLT-trees. So the size
of these generalized SLT-trees, i.e. the number of edges (except for the dotted edges) in
the trees, represents the major part of its computational complexity. Since each edge in an
SLT-tree is generated by applying either a program clause or a tabled answer, the size of a
generalized SLT-tree is the number of applications of program clauses and tabled answers
during the resolution.
The following notation is borrowed from [7].
Definition 5.1 Let P be a program. Then |P | denotes the number of clauses in P , and ΠP
denotes the maximum number of literals in the body of a clause in P . Let s be an arbitrary
positive integer. Then N(s) denotes the number of atoms of predicates in P that are not
variants of each other and whose arguments do not exceed s in size.
Theorem 5.5 Let P be a program with the bounded-term-size property, G0 =← A be a top
goal (with A an atom), and CS be a fixed depth-first control strategy. Then the size of each
generalized SLT-tree GTGi 0 is O(|P |N(s)ΠP +2 ) for some s > 0.
Proof: Let n be the maximum size of arguments in A. Since P has the bounded-term-size
property, neither subgoal nor tabled answer has arguments whose size exceeds f (n) for some
function f . Let s = f (n). Then the number of distinct subgoals (up to variable renaming)
in GTGi 0 is bounded by N(s).
Let B = p(.) be a subgoal. By Theorem 5.4, each clause Cpj will be applied to all variant
subgoals of B in GTGi 0 at most N(s) + 1 times. So the number of applications of all program
clauses to all selected subgoals in GTGi 0 is bounded by
N(s) ∗ |P | ∗ (N(s) + 1)

(6)
38

Moreover, when a program clause is applied, it introduces at most ΠP subgoals. Since the
number of tabled answers to each subgoal is bounded by N(s), the ΠP subgoals access at
most N(s)ΠP times to tabled answers. Hence the number of applications of tabled answers
to all subgoals in GTGi 0 is bounded by
N(s) ∗ |P | ∗ (N(s) + 1) ∗ N(s)ΠP

(7)

Therefore the size of GTGi 0 is bounded by (6) + (7), i.e. O(|P |N(s)ΠP +2 ). ✷
The second part of the computational complexity of SLT-resolution comes from loop
checking, which occurs during the determination of looping clauses (see point 3 of Definition 3.3). Let Ak = p(.) be a selected subgoal at node Nk in GTGi 0 and ALAk =
{(Nk−1 , Ak−1), ..., (N0 , A0 )} be its ancestor list. For convenience we express the ancestordescendant relationship in ALAk as a path like
N0 : A0 ⇒CA0 ...Nj : Aj ⇒CAj ...Nk−1 : Ak−1 ⇒CAk−1 Nk : Ak

(8)

where CAj is a program clause used by Aj . By Definitions 3.1 and 3.2, N0 is the root of
GTGi 0 and Aj is an ancestor subgoal of Aj+l (0 ≤ j < k, l > 0). If Aj is a variant of Ak , a
loop occurs between Nj and Nk so that the looping clause CAj will be skipped by Ak .
It is easily seen that k subgoal comparisons may be made to check if Ak has ancestor
variants. So if we do such loop checking for every Aj in the path, then we may need O(K 2 )
comparisons.
By Optimization 3 program clauses are selected in a fixed order which is specified by
a fixed control strategy. Let all clauses with head predicate p be selected in the order:
Cp1 , Cp2 , ..., Cpm . Then Ak and all its ancestor variant subgoals should follow this order.
Assume Aj is the closest ancestor variant subgoal of Ak in the path (8). Let CAj = Cpl .
Then by Optimization 3 each Cph (h < l) either is a looping clause of Aj or has been
completely used by a variant of Aj . This applies to Ak as well. So Ak should skip all Cph s
(h ≤ l). This shows the following important fact.
Fact 1 To determine looping clauses or clauses that have been completely used for Ak , it
suffices to find the closest ancestor variant subgoal of Ak .
Theorem 5.6 Let P be a program with the bounded-term-size property, G0 =← A be a top
goal (with A an atom), and CS be a fixed depth-first control strategy. Then the number of
subgoal comparisons performed in searching for the closest ancestor variant subgoals of all
selected subgoals in each generalized SLT-tree GTGi 0 is O(|P |N(s)3).
Proof: Note that loop checking only relies on ancestor lists of subgoals, which only depend
on program clauses with non-empty bodies (see Definition 3.1). By formula (6) in the
39

proof of Theorem 5.5, the total number of applications of program clauses to all selected
subgoals in GTGi 0 is bounded by N(s) ∗ |P | ∗ (N(s) + 1). Since each subgoal in the ancestordescendant path (8) has at most |P | ancestor variant subgoals (i.e. the first variant uses the
first program clause, the second uses the second, ..., and the |P |-th uses the last program
clause), the length of the path is bounded by N(s) ∗ |P |. Assume in the worst case that all
N(s) ∗ |P | ∗ (N(s) + 1) applications of clauses generate N(s) + 1 ancestor-descendant paths
like (8) of length N(s) ∗ |P |. Since each subgoal in a path needs at most N(s) comparisons to
find its closest ancestor variant subgoal, the number of comparisons for all subgoals in each
path is bounded by N(s) ∗ |P | ∗ N(s). Therefore, the total number of subgoal comparisons
in N(s) + 1 paths is bounded by
N(s) ∗ |P | ∗ N(s) ∗ (N(s) + 1)

(9)

i.e. O(|P |N(s)3). ✷
Combining Theorems 5.5 and 5.6 and Fact 1 leads to the following.
Theorem 5.7 The time complexity of SLT-resolution is O(|P |N(s)ΠP +3 logN(s)).
Proof: The time complexity of SLT-resolution consists of the part of accessing program
clauses, which is formula (6) times the complexity of accessing one clause, the part of accessing tabled answers, which is formula (7) times the complexity of accessing one tabled
answer, and the part of subgoal comparisons in loop checking, which is formula (9) times the
complexity of comparing two subgoals. The access to one program clause and the comparison
of two subgoals can be assumed to be in constant time. A global table of subgoals and their
answers can be maintained, so that the time for retrieving and inserting a tabled answer
can be assumed to be O(logN(s)). So the time complexity of constructing one generalized
SLT-tree GTGi 0 is
O((6) + (7) ∗ logN(s) + (9)) = O(|P |N(s)ΠP +2 logN(s))

(10)

Since the number of GTGi 0 s, i.e. the number of recursions of SLT-resolution, is bounded by
N(s) (since each GTGi 0 produces at least one new tabled answer), the time complexity of
SLT-resolution is O(|P |N(s)ΠP +3 logN(s)). ✷
It is shown in [33] that the data complexity of the well-founded semantics, as defined by
Vardi [34], is polynomial time for function-free programs. This is obviously true with SLTresolution because in this case, s = 1 and N(1) is a polynomial in the size of the extensional
database (EDB) [7].

40

6

Related Work

So far only two operational procedures for top-down evaluation of the well-founded semantics
of general logic programs have been extensively studied: Global SLS-resolution and SLGresolution. Global SLS-resolution is not effective since it is not terminating even for functionfree programs [18, 22]. Therefore, in this section we make a detailed comparison of SLTresolution with SLG-resolution.
There are three major differences between these two approaches. First, SLG-resolution
is based on program transformations, instead of on standard tree-based formulations like
SLDNF- or Global SLS-resolution. Starting from the predicates of the top goal, it transforms (instantiates) a set of clauses, called a system, into another system based on six basic
transformation rules. A special class of literals, called delaying literals, is used to represent and handle temporarily undefined negative literals. Negative loops are identified by
maintaining a dependency graph of subgoals [6, 7]. In contrast, SLT-resolution is based on
SLT-trees in which the flow of the query evaluation is naturally depicted by the ordered
expansions of tree nodes. It appears that this style of formulations is easier for users to
understand and keep track of the computation. In addition, SLT-resolution handles temporarily undefined negative literals simply by replacing them with u∗ , and treats positive
and negative loops in the same way based on ancestor lists of subgoals.
The second difference is that like all existing tabling methods, SLG-resolution adopts the
solution-lookup mode. Since all variant subgoals acquire answers from the same source − the
solution node, SLG-resolution essentially generates a search graph instead of a search tree,
where every lookup node has a hidden edge towards the solution node, which demands the
solution node to produce new answers. Consequently it has to jump back and forth between
lookup and solution nodes. This is the reason why SLG-resolution is not linear for query
evaluation. In contrast, SLT-resolution makes linear tabling derivations by generating SLTtrees. SLT-trees can be viewed as SLDNF-trees with no infinite loops and with significantly
less redundant sub-branches.
Since SLG-resolution deviates from SLDNF-resolution, some standard Prolog techniques
for the implementation of SLDNF-resolution, such as the depth-first control strategy and
the efficient stack-based memory management,6 cannot be used for its implementation. This
shows a third essential difference. SLT-resolution bridges the gap between the well-founded
semantics and standard Prolog implementation techniques, and can be implemented by an
extension to any existing Prolog abstract machines such as WAM or ATOAM.
The major shortcoming of SLT-resolution is that it is a little more time costly than SLGresolution. The time complexity of SLG-resolution is O(|P |N(s)ΠP +1 logN(s)) [7], whereas
ours is O(|P |N(s)ΠP +3 logN(s)) (see Theorem 5.7). The extra price of our approach, i.e.
6

Bol and Degerstedt [3] defined a special depth-first strategy that may be suitable for SLG-resolution.
However, their definition of “depth-first” is quite different from the standard one used in Prolog [15, 16].

41

O(N(s)) recursions (see Definition 3.7) and O(N(s)) applications of each program clause to
each distinct (up to variable renaming) subgoal (see Theorem 5.4), is paid for the preservation
of the linearity for query evaluation. It should be pointed out, however, that in practical
situations, the number of recursions and that of clause applications are far less than O(N(s)).
We note that in many typical cases, such as Examples 3.2, 5.2 and 5.5, both numbers are less
than 3. Moreover, the efficiency of SLT-resolution can be further improved by completing
its recursions locally; see [27] for such special techniques.
Finally, for space consumption we note that SLG-resolution takes much more space than
SLT-resolution. The solution-lookup mode used in SLG-resolution requires that solution
nodes stay forever whenever they are generated even if they will never be invoked later. In
contrast, SLT-resolution will easily reclaim the space through backtracking using the efficient
stack-based memory structure.

7

Conclusion

We have presented a new operational procedure, SLT-resolution, for the well-founded semantics of general logic programs. Unlike Global SLS-resolution, it is free of infinite loops
and with significantly less redundant sub-derivations; it terminates for all programs with the
bounded-term-size property. Unlike SLG-resolution, it preserves the linearity of SLDNFresolution, which bridges the gap between the well-founded semantics and standard Prolog
implementation techniques.
Prolog has many well-known nice features, but the problem of infinite loops and redundant computations considerably undermines its beauties. The general goal of our research
is then to extend Prolog with tabling to compute the well-founded semantics while resolving
infinite loops and redundant computations. SLT-resolution serves as a nice model for such
an extension. (Note that XSB [23, 25] is the only existing system that top-down computes
the well-founded semantics of general logic programs, but it is not an extension of Prolog
since SLG-resolution and SLDNF-resolution are totally heterogeneous.)
For positive programs, we have developed special methods for the implementation of
SLT-resolution based on the control strategy used by Prolog [27]. The handling of cuts of
Prolog is also discussed there. A preliminary report on methods for the implementation of
SLT-resolution for general logic programs appears in [28].

Acknowledgements
The first author is supported in part by Chinese National Natural Science Foundation and
Trans-Century Training Program Foundation for the Talents by the Chinese Ministry of
Education.

42

A

Optimized SLT-Trees

Assume that program clauses and tabled answers are stored separately, and that new tabled
positive answers in SLT-trees are added into the table T Bt once they are generated (see
Section 5.3). Combining Optimizations 1, 2 and 3 in Section 5 with Definition 3.3, we
obtain an algorithm for generating optimized SLT-trees based on a fixed depth-first control
strategy.
Definition A.1 (SLT-trees, an optimized version) Let P = P c ∪ T Bt be a program
with P c a set of program clauses and T Bt a set of tabled positive answers. Let G0 be a top
goal and CS be a depth-first control strategy. Let T Bf be a set of ground atoms such that
for each A ∈ T Bf ¬A ∈ W F (P ). The optimized SLT-tree TG0 for (P ∪ {G0 }, T Bf ) via CS
is a tree rooted at node N0 : G0 , which is generated as follows.
1. Select the root node for expansion.
2. (Node Expansion) Let Ni : Gi be the node selected for expansion, with Gi =←
L1 , ..., Ln .
(a) If n = 0 then mark Ni by ✷t (a success leaf) and goto 3 with N = Ni .
(b) If L1 = u∗ then mark Ni by ✷u∗ (a temporarily undefined leaf) and goto 3 with
N = Ni .
(c) Let Lj be a positive literal selected by CS. Select a tabled answer or program
clause, C, from P based on CS while applying Optimizations 2 and 3. If C is
empty, then if Ni has already had child nodes then goto 3 with N = Ni else mark
Ni by ✷f (a failure leaf) and goto 3 with N = Ni . Otherwise, Ni has a new child
node labeled by the resolvent of Gi and C over the literal Lj . Select the new child
node for expansion and goto 2.
(d) Let Lj = ¬A be a negative ground literal selected by CS. If A is in T Bf then Ni
has only one child that is labeled by the goal ← L1 , ..., Lj−1, Lj+1 , ..., Ln , select
this child node for expansion, and goto 2. Otherwise, build an optimized SLT-tree
T←A for (P ∪ {← A}, T Bf ) via CS, where the subgoal A at the root inherits the
ancestor list ALLj of Lj . We consider the following cases:
i. If T←A has a success leaf then mark Ni by ✷f and goto 3 with N = Ni ;
ii. If the root of T←A is loop-independent and all branches of T←A end with
a failure leaf then Ni has only one child that is labeled by the goal ←
L1 , ..., Lj−1, Lj+1 , ..., Ln , select this child node for expansion, and goto 2;
iii. Otherwise, Ni has only one child that is labeled by the goal ← L1 , ..., Lj−1 , Lj+1 ,
..., Ln , u∗ if Ln 6= u∗ or ← L1 , ..., Lj−1 , Lj+1 , ..., Ln if Ln = u∗ . Select this child
node for expansion and goto 2.
43

3. (Backtracking) If N is loop-independent and the selected literal A at N is positive
then set comp(A) = Y es. If N is the root node then return. Otherwise, let Nf : Gf be
the parent node of N, with the selected literal Lf . If Lf is negative then goto 3 with
N = Nf . Else, if N was generated from Nf by resolving Gf with a program clause C
on Lf then set comp used(Lf , C) = Y es. Select Nf for expansion and goto 2.
Optimization 1 is used at item 2(d)ii. Optimizations 2 and 3 are applied at item 2c for
the selection of program clauses. The flags comp( ) and comp used( , ) are updated during
backtracking (point 3). The flag loop depend( ) is assumed to be updated automatically
based on loop dependency of nodes.

References
[1] K. R. Apt, M. H. Van Emden, Contributions to the theory of logic programming, J.
ACM 29(3):841-862 (1982).
[2] R. N. Bol, K. R. Apt and J. W. Klop, An analysis of loop checking mechanisms for logic
programs, Theoretical Computer Science 86(1):35-79 (1991).
[3] R. N. Bol and L. Degerstedt, The underlying search for magic templates and tabulation,
in: Proc. of the Tenth International Conference on Logic Programming, MIT Press,
1993.
[4] R. N. Bol and L. Degerstedt, Tabulated resolution for the well-founded semantics. Journal of Logic Programming 34(2):67-109 (1998).
[5] D. Chan, Constructive negation based on the completed database, in: (R. A. Kowalski
and K. A. Bowen, eds.) Proc. of the Fifth International Conference and Symposium on
Logic Programming, Seattle, USA, MIT Press, 1988, pp. 111-125.
[6] W. D. Chen, T. Swift and D. S. Warren, Efficient top-down computation of queries
under the well-founded semantics, Journal of Logic Programming 24(3):161-199 (1995).
[7] W. D. Chen and D. S. Warren, Tabled evaluation with delaying for general logic programs, J. ACM 43(1):20-74 (1996).
[8] K. L. Clark, Negation as Failure, in: (H. Gallaire and J. Minker, eds.) Logic and
Databases, Plenum, New York, 1978, pp. 293-322.
[9] D. De Schreye and S. Decorte, Termination of logic programs: the never-ending story,
Journal of Logic Programming 19/20:199-260 (1993).

44

[10] W. Drabent, What is failure? An approach to constructive negation, Acta Informatica
32(1):27-59 (1995).
[11] M. Gelfond and V. Lifschitz, The stable model semantics for logic programming, in: (R.
A. Kowalski and K. A. Bowen, eds.) Proc. of the Fifth International Conference and
Symposium on Logic Programming, Seattle, USA, MIT Press, 1988, pp. 1070-1080.
[12] R. A. Kowalski and D. Kuehner, Linear resolution with selection functions, Artificial
Intelligence 2:227-260 (1971).
[13] R. A. Kowalski, Predicate logic as a programming language, IFIP 74, pp.569-574.
[14] J. Y. Liu, L., Adams, and W. Chen, Constructive negation under the well-founded
semantics, Journal of Logic Programming 38(3):295-330 (1999).
[15] J. W. Lloyd, Foundations of Logic Programming, 2nd ed., Springer-Verlag, Berlin, 1987.
[16] U. Nilsson and J. Maluszynski, Logic Programming and Prolog, 2nd ed., John Wiley &
Sons, 1995.
[17] T. Przymusunski, On the declarative and procedural semantics of logic programs, Journal of Automated Reasoning 5:167-205 (1989).
[18] T. Przymusunski, Every logic program has a natural stratification and an iterated fixed
point model, in: Proc. of the 8th ACM Symposium on Principles of Database Systems,
1989, pp. 11-21.
[19] T. Przymusunski, On constructive negation in logic programming, in: (E. L. Lusk and
R. A. Overbeek eds.) Proc. of the North American Conference on Logic Programming,
Ohi, USA, MIT Press, 1989, page (Addendum to the Volume).
[20] T. Przymusunski, The well-founded semantics coincides with the three-valued stable
semantics, Fundamenta Informaticae 13:445-463 (1990).
[21] J. A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM
12(1):23-41 (1965).
[22] K. Ross, A procedural semantics for well-founded negation in logic programs, Journal
of Logic Programming 13(1):1-22 (1992).
[23] K. Sagonas, T. Swift and D. S. Warren, XSB as an efficient deductive database engine,
in: Proc. of the ACM SIGMOD Conference on Management of Data, Minneapolis, 1994,
pp. 442-453.

45

[24] K. Sagonas and T. Swift, An abstract machine for tabled execution of fixed-order stratified logic programs, ACM Transactions on Programming Languages and Systems, 20(3)
(1998).
[25] K. Sagonas, T. Swift, D. S. Warren, J. Freire and P. Rao, The XSB Programmer’s
Manual (Version 1.8), 1998.
[26] Y. D. Shen, An extended variant of atoms loop check for positive logic programs, New
Generation Computing 15(2):187-204 (1997).
[27] Y. D. Shen, L. Y. Yuan, J. H. You, and N. F. Zhou, Linear tabulated resolution based on
Prolog control strategy, Theory and Practice of Logic Programming (previously Journal
of Logic Programming), to appear.
[28] Y. D. Shen, L. Y. Yuan, J. H. You and N. F. Zhou, Linear tabulated resolution for
the well founded semantics, in: Proc. of the 5th International Conference on Logic
Programming and Nonmonotonic Reasoning, Texas USA, 1999, pp. 192-205.
[29] J. C. Shepherdson, Negation in logic programming, in: (J. Minker, ed.) Foundations of
Deductive Databases and Logic Programming, Morgan Kaufmann, 1988, pp. 19-88.
[30] H. Tamaki and T. Sato, OLD resolution with tabulation, in: Proc. of the Third International Conference on Logic Programming, London, 1986, pp. 84-98.
[31] M. H. Van Emden and R. A. Kowalski, The semantics of predicate logic as a programming language, J. ACM 23(4):733-742 (1976).
[32] A. Van Gelder, Negation as failure using tight derivations for general logic programs,
Journal of Logic Programming 6(1&2):109-133 (1989).
[33] A. Van Gelder, K. Ross, J. Schlipf, The well-founded semantics for general logic programs, J. ACM 38(3):620-650 (1991).
[34] M. Vardi, The complexity of relational query languages, in: ACM Symposium on Theory
of Computing, 1982, pp. 137-146.
[35] L. Vieille, Recursive query processing: the power of logic, Theoretical Computer Science
69:1-53 (1989).
[36] D. H. D. Warren, An abstract Prolog instruction set, Technical Report 309, SRI International, 1983.
[37] D. S. Warren, Memoing for logic programs, CACM 35(3):93-111 (1992).

46

[38] N. F. Zhou, Parameter passing and control stack management in Prolog implementation
revisited, ACM Transactions on Programming Languages and Systems, 18(6):752-779
(1996).

47

