Computation of Stable Models and Its Integration with Logical Query Processing.
AbstractThe well-founded semantics and the stable model semantics capture intuitions of the skeptical and credulous semantics in nonmonotonic reasoning, respectively. They represent the two dominant proposals for the declarative semantics of deductive databases and logic programs. However, neither semantics seems to be suitable for all applications. We have developed an efficient implementation of goal-oriented effective query evaluation under the well-founded semantics. It produces a residual program for subgoals that are relevant to a query, which contains facts for true instances and clauses with body literals for undefined instances. This paper presents a simple method of stable model computation that can be applied to the residual program of a query to derive answers with respect to stable models. The method incorporates both forward and backward chaining to propagate the assumed truth values of ground atoms, and derives multiple stable models through backtracking. Users are able to request that only stable models satisfying certain conditions be computed. A prototype has been developed that provides integrated query evaluation under the well-founded semantics, the stable models, and ordinary Prolog execution. We describe the user interface of the prototype and present some experimental results.
Introduction
Significant progress has been made in understanding the declarative semantics of deductive
databases and logic programs with negation. Two dominant proposals are the well-founded
semantics [31] and the stable model semantics [13]. For a normal logic program, where the body
of each rule is a conjunction of literals, its well-founded semantics is characterized by a unique
Supported in part by the National Science Foundation under Grant No. IRI-9212074.
y Supported in part by the National Science Foundation under Grant No. CCR-9102159.
three-valued model, called the well-founded partial model. It is well defined for all normal logic
programs. However, the well-founded semantics is inadequate in dealing with reasoning by cases
or multiple alternative situations.
Example 1.1 Consider the following program:
covered(Course) :- teach(Faculty, Course).
Its well-founded partial model is such that every ground atom is undefined, thus providing no
useful information about the scenario being described. 2
The well-founded semantics of normal logic programs has been extended by Van Gelder [30]
to general logic programs, where the body of each rule may be an arbitrary first-order formula.
The resulting semantics is called the alternating fixpoint logic [30].
The notion of stable models [13] originated from the work on autoepistemic logic [12]. Each
stable model represents a set of beliefs that can be derived from itself. In Example 1.1, there are
two stable models, one in which John teaches CSE 5381 and the other in which Mary teaches
CSE 5381. In either case, CSE 5381 is covered. Unlike the well-founded partial model, stable
models may not exist for a given program, e.g., p :-p, and even if they exist, they may not be
unique.
Recent research shows that the well-founded partial model and (two-valued) stable models
are two extreme cases of three-valued stable models [9, 22, 26]. The well-founded partial model
coincides with the smallest three-valued stable model. It corresponds to the skeptical semantics
that includes only beliefs that are true in all possible situations. On the other hand, the notion
of stable models captures the credulous semantics that concludes as many beliefs as possible from
a normal logic program.
Separate techniques have been developed for query evaluation under the well-founded semantics
and for computing stable models. The well-founded semantics has a constructive definition
based upon a least fixpoint construction. For function-free programs, it has a polynomial time
data complexity [31]. In addition to direct extensions of SLDNF resolution [21, 24], various
mechanisms of positive and negative loop handling have been incorporated for effective query
evaluation under the well-founded semantics [2, 3, 6, 7, 23, 28]. However, not all of them can be
extended directly for stable model computation.
The definition of stable models requires guessing an interpretation and then verifying if it is
a stable model. In fact, the problem of the existence of a stable model of a logic program is NP-complete
[17]. There have been several proposals for stable model computation [10, 19, 20, 26].
Two aspects are common. One is that only two-valued stable models are computed. This is
not surprising. Two-valued stable models represent the credulous semantics that does not allow
any incomplete information, and they have a smaller search space from a computational point
of view. The other common aspect is that only ground programs are processed. This, however,
is a severe restriction in practice since almost all rules have variables.
We have developed a prototype system, called SLG, for logical query answering. SLG supports
goal-oriented query evaluation under the well-founded semantics of normal logic programs, or
more generally, the alternating fixpoint logic of general logic programs. The latter is an important
extension since a standard translation of general logic programs into normal logic programs does
not always preserve the semantics. In either case, SLG has a polynomial time data complexity
for function-free programs. If a query has undefined instances, SLG produces a residual program
besides true and false instances of the query. The residual program can be further processed to
compute its (two-valued) stable models. SLG is available by anonymous ftp from seas.smu.edu
or cs.sunysb.edu.
By applying stable model computation to only the residual program of a query, SLG has two
advantages. First, answers of a query that are true in the well-founded semantics can always
be derived within polynomial time in the size of a database. They can be computed even more
efficiently if a program satisfies certain properties such as stratification. More importantly, non-ground
programs and queries can be handled. Second, the residual program of a query is often
much smaller than the original program. The approach in SLG restricts the potentially expensive
(two-valued) stable model computation to a small portion of the entire program. Furthermore,
three-valued stable models are partially supported since the original program may not have a
(two-valued) stable model even though the portion of the program that is relevant to a query
has (two-valued) stable models.
The main contributions of this paper are threefold. First, we describe a simple assume-and-
reduce algorithm for computing (two-valued) stable models of a finite ground program. It assumes
the truth values of only those ground atoms whose negative counterparts occur in a program.
The search space of stable models is further reduced by forward and backward propagation of
the assumed truth values of ground atoms and by reduction of the program. Second, we show
how to integrate query evaluation under the well-founded semantics with the computation of
stable models. Two aspects are noteworthy. One is that handling negative loops by delaying
not only avoids redundant derivations, but also leads to the residual program needed for stable
model computation later. The other is that the forward chaining network set up for simplifying
delayed literals in the derivation of the well-founded semantics is directly useful for stable model
computation. Finally, due to the multitude of stable models, it is not clear what answers should
be computed for a query. We introduce a versatile user interface for query evaluation with respect
to stable models.
Section 2 describes a method of stable model computation. Section 3 presents its integration
with query evaluation of the well-founded semantics. Section 4 contains some examples and
performance analysis. Section 5 compares with related work.
2 Computation of Stable Models
This section reviews the terminologies of logic programs [16] and the notion of (two-valued)
stable models by Gelfond and Lifschitz [13]. An assume-and-reduce algorithm is described for
computing (two-valued) stable models of finite ground programs.
2.1 Definition of Stable Models
An atom is of the form p(t 1
is an n-ary predicate symbol and t 1
are terms.
For an atom A, A is a positive literal and -A is a negative literal, and they are complements of
each other. A clause is of the form
A :-
where A, the head of the clause, is an atom, and the body of the clause, are
literals. A definite clause is a clause that has no negative literals in its body. A (definite) program
is a set of (definite) clauses. A ground atom (literal, clause, program) is one that is variable-free.
The Herbrand universe of a program P is the set of all ground terms that may be constructed
from the constants and function symbols appearing in P . An arbitrary constant is added if no
constant occurs in P . The Herbrand base of P , denoted by B P , is the set of all ground atoms with
predicates occurring in P whose arguments are in the Herbrand universe of P . The Herbrand
instantiation of P is the (possibly infinite) set of all ground clauses obtained by substituting
terms in the Herbrand universe for variables in clauses in P .
A set I of ground literals is consistent if for no ground atom A, both A and -A are in I.
We denote by P os(I) the set of positive literals in I and Neg(I) the set of ground atoms whose
complements are in I. A partial interpretation (or just interpretation) I is a consistent set of
ground literals. A total interpretation is an interpretation where
ground literal L is true in an interpretation I if and only if L 2 I.
Definition 2.1 ([13]) Let P be a program and I be an interpretation. The Gelfond-Lifschitz
transformation of P with respect to I, denoted by P I , is the program obtained from the Herbrand
instantiation of P by deleting
ffl each clause that has a negative literal -B in its body with B 2 I, and
ffl all negative literals -B in the bodies of the remaining clauses with -B 2 I.
If I is a total interpretation, the resulting program P I is a definite program. According to [1],
every definite program P has a unique minimal model, which we will denote by M(P ).
Definition 2.2 ([13]) Let I be a total interpretation, and P be a logic program. I is a (two-
valued) stable model of P if and only if I coincides with M(P I ).
2.2 Derivation of Stable Models
For the derivation of stable models, we consider finite ground programs. The application for
goal-oriented query evaluation of non-ground logic programs will be discussed in Section 3.
Let P be a finite ground program. We can restrict interpretations to ground atoms that occur
in P as every ground atom that does not occur in P is definitely false. According to Definition
2.2, stable models of P can be computed by enumerating every possible total interpretation I
and checking if I coincides with the unique minimal model M(P I ) of P I . The number of possible
total interpretations is obviously exponential in the size of the Herbrand base. Fortunately there
are often mutual dependencies among ground atoms in a program, which can be used to reduce
the search space and to speed up the computation of stable models substantially.
2.2.1 Assuming Negative Literals Only
Our first observation is that we have to guess only the truth values of ground atoms A such that
-A occurs in P .
Example 2.1 Consider the following ground program:
Two negative literals, -teach(mary,cse5381) and -teach(john,cse5381), occur in the program.
As soon as their truth values are determined, the truth value of covered(cse5381) can be derived.
There is no need to make assumptions about the truth value of covered(cse5381). This reduces
the search space for stable models. 2
Let N (P ) denote the set of ground atoms A such that -A occurs in P .
Lemma 2.1 Let P be a ground logic program, and I be a total interpretation. Then I is a
stable model of P if and only if for some interpretation J , where
I coincides with M(P J ).
Proof: Let I be a total interpretation and let J be the restriction of I to N (P
and the lemma follows from the
definition of stable models. 2
2.2.2 Propagation of Assumed Truth Values
The truth values of ground atoms in N (P ) are not independent of each other either. In Example
2.1, if we assume that teach(mary,cse5381) is true, the clause for teach(john,cse5381) can be
deleted since its body is false according to the assumption. Hence teach(john,cse5381) must be
false. Similarly, if teach(mary,cse5381) is assumed to be false, teach(john,cse5381) can be derived
to be true. Therefore it is not necessary to enumerate all the four possible truth assignments for
teach(john,cse5381) and teach(mary,cse5381).
Our second observation is that the assumed truth value of a ground atom should be used to
simplify the program being considered in order to reduce the search space for truth assignments
of ground atoms in N (P ) that lead to stable models.
Let P be a finite ground program, and -A be a ground literal that occurs in P . There are
two possible choices: either A is true or -A is true. We derive two programs from P , namely PA
where P is simplified based upon the assumption that A is true and P-A where P is simplified
based upon the assumption that -A is true. The objective is to derive stable models of P from
those of PA and P-A .
The simplification of a program P based upon the assumed truth value of a literal should be
done in such a way that avoids the generation of models that are supported but not stable.
Example 2.2 Let P be the following program:
The only stable model for P , which is also the perfect model in this case, is that q is true and p
is false. Suppose that p is assumed to be true. Based upon the assumption that p is true, we can
delete the clause for q since -p is false according to the assumption. However, the assumption
that p is true cannot be used to simplify away the positive occurrence of p in the body of the
clause for p. Otherwise, we would derive a model, fp; -qg, that is not a stable model. Therefore
the simplified program, P p , should contain one clause, p :- p. In this particular case, assuming
that p is true does not lead to any stable model since p is false in the stable model of P p , which
is inconsistent with the assumption.
On the other hand, suppose that -p is assumed to be true. The simplified program, P-p ,
should contain one fact, q. That is, the assumption that -p is true can be used to delete the
clause for p since its body is false according to the assumption. 2
Example 2.2 indicates that the assumed truth value of a ground atom can be used to delete
every clause whose body is false and every negative body literal that is true according to the
assumption, but it cannot be used to delete a positive body literal that is assumed to be true.
Definition 2.3 Let P be a ground program, and L be a ground literal. Then PL is the program
obtained from P by deleting
ffl every clause in P whose body contains the complement of L, and
ffl every occurrence of L in P if L is a negative literal.
Lemma 2.2 Let P be a ground program, A be a ground atom, and I be a total interpretation.
Then I is a stable model of P if and only if either A is true in I and I is a stable model of PA ,
or -A is true in I and I is a stable model of P-A .
Proof: Suppose that A is true in I. Then P Therefore I is a stable model of P if and
only if I is a stable model of PA .
Now assume that -A is true in I. Compared with Gelfond-Lifschitz transformation, the
simplification of P to P-A also deletes all clauses that have a positive literal A in the body.
Therefore P I is identical to (P-A ) I , except that P I may contains some additional clauses with
positive literal A in the body. By definition, I is a stable model of P if and only if I coincides
with M(P I ). Since -A is true in I, A must be false in M(P I ). Therefore M(P I
and so I is a stable model of P if and only if I is a stable model of P-A . 2
2.2.3 Reduction of a Program
Our third observation is that the simplification carried out by the construction of PL may determine
the truth values of other ground atoms, which should be propagated as much as possible to
reduce the program for which stable models are being sought. The propagation allows us to avoid
choice points for guessing truth values of ground atoms whose values are already determined by
previous assumptions.
Example 2.3 Let P be the following program on the left:
q :-s. q :-s.
q :-u. q.
r :-t. r :-t.
Suppose that -u is assumed to be true. The program, P-u , obtained from P , is shown above
on the right. Further propagation of known truth values of ground atoms leads to a partial
interpretation, namely fp; q; -s; -u; vg, and a much simpler program:
r :-t.
In this case, the derived truth value of u is consistent with the assumption that -u is true. 2
Propagation of previously known or assumed truth values is essentially a process of forward
chaining. The result is a partial interpretation and a reduced program.
Definition 2.4 Let P be a ground program, and U be a set of ground atoms that contains all
those occurring in P . We define I
only if
ffl I is a non-empty interpretation, where P os(I) is the set of all ground atoms A such that
contains a fact A, and Neg(I) is the set of all ground atoms A in U such that there is
no clause in P with A in the head, and
is obtained from P by deleting
- every clause that has a literal L in the body that is false in I, and
- every literal L in the bodies of remaining clauses such that L is true in I, and then
- every clause with A in the head where A 2 P os(I).
is reduced if there exists no interpretation I such that (P; U) I
U 0 .
Notice that if (P; U) is not reduced, there exists a unique non-empty interpretation I, a unique
I
is reduced, then U must be exactly the set of all
atoms occurring in P .
In Example 2.3, let U 0
be fp; q;
is fp; q; vg,
and
contains the following two clauses:
r :-t.
and U 1 is fr; s; t; ug. With another step of reduction, we have
I reduction is possible since
reduced.
Definition 2.5 Let P be a ground program, and U(P ) be the set of all ground atoms occurring
in P . P is reduced to an interpretation I and a program P 0 if and only if for some n - 0,
\Gamma! ::: In
\Gamma!
where
Notice that every finite ground program can be reduced to an interpretation and a (possibly
simpler) program. The following lemma shows that reduction preserves stable models.
Lemma 2.3 Let P be a finite ground program, and P be reduced to an interpretation I   and a
program P   . Then every stable model I of P is equal to I   [ J for some stable model J of P
and vice versa. Furthermore, if P is a definite program, then P os(I
Proof: We show that every step of reduction preserves stable models, and the lemma follows by
a simple induction.
Suppose that (P k ; U k ) I k+1
consists of all ground atoms
A where A is a fact in P k , and Neg(I k+1 ) consists of all ground atoms A 2 U where there is no
clause in P k with A in the head.
Let I be any interpretation such that P os(I) [
interpretation J where
For any interpretation I such that P os(I) [ I is a stable model of P k if and
only if I
and is a stable model of P k+1 . 2
The reduction of a program with respect to a partial interpretation differs from the simplification
of a program according to the assumed truth value of a ground atom. Recall that if a
ground atom A is assumed to be true, this assumption cannot be used to delete any occurrence
of A in a program as a clause body literal. On the other hand, the reduction of a program P
with respect to a partial interpretation I is similar to the bottom-up computation embodied in
the transformation T P (I) [1].
Reduction, however, does not attempt to compute the well-founded semantics. It derives only
literals that are true or false with respect to Clark's completion of a program. For instance, the
following program
cannot be reduced further. In our framework, reduction is used in stable model computation,
which is carried out after a query is evaluated under the well-founded semantics. There is no
interleaving of computations of stable models and the well-founded semantics, in the sense that
our algorithm of stable model computation does not call any general procedure for computing
the well-founded semantics.
2.3 Assume-and-Reduce Algorithm

Figure

1 shows the assume-and-reduce algorithm for computing stable models of a finite ground
program. The algorithm is non-deterministic in the sense that certain choices have to be made
at some point. However, all stable models can be enumerated through backtracking.
Input: a finite ground program P
Output: a stable model or failure
begin
Let P be reduced to an interpretation I 0 and a program P
(3) AI := ;; N := N(Pgm);
(4) while N 6= ; do begin
(5) Delete an arbitrary element, A, from N ;
if A 62 DI and -A 62 DI then begin
choice point: L can be either A or -A */
AI := AI [fLg;
Let PgmL be reduced to an interpretation I   and a program P   ;
inconsistent then
AI and A 62 DI for some ground atom A then
else begin
(18) for every A that occurs in Pgm, add -A to DI;
return AI [ DI as a stable model of P ;

Figure

1: The assume-and-reduce algorithm for computing stable models
Theorem 2.4 Let P be a finite ground program. Then an interpretation I is a stable model of
P if and only if I is returned by an execution of the assume-and-reduce algorithm.
Proof: In the algorithm, DI represents the set of ground literals that have been derived to
be true (possibly from previous assumptions), and AI represents the set of ground literals that
are assumed to be true. The algorithm explores a tree of search space for stable models in a
non-deterministic and backtracking manner, where each node can be represented by a triple
(AI; DI;P gm). It terminates for finite ground programs.
We prove that the search space explored by the assume-and-reduce algorithm is complete.
Initially, the root node of the search tree is (AI; DI;P is reduced to
I 0 and P 0 . By Lemma 2.3, I is a stable model of P if and only if I = I 0 [ J and J is a stable
model of P 0 , i.e., I = AI [ DI [ J , where J is a stable model of P gm.
Given a node v represented by (AI; DI;P gm), let A be any ground atom in N (P ), i.e., -A
occurs in P , such that neither A or -A is in AI [ DI. Then -A is still in P gm. There are two
choices, either A is true or -A is true. By Lemma 2.2, an interpretation J is a stable model of
only if either A is true in J and J is a stable model of P gmA , or -A is true in J and
J is a stable model of P gm-A . Let P gmA (P gm-A ) be reduced to an interpretation I
A
-A
and a program P
A (P
-A ). Again, by Lemma 2.3, J is a stable model of P gmL , where L can be
either A or -A, if and only if
, where J
is a stable model of P
. Then v has two
child nodes. One is (AI [
A ) and the other is (AI [ f-Ag;DI [ I
-A ). By
the arguments above, for any interpretation I, I = AI [DI [J for some stable model J of P gm
if and only if for L that can be either A or -A, L 2 J and
L for some stable model
L of P
L for some stable model J
L of P
L .
For a leaf node v represented by (AI; DI;P gm) in the search tree for stable models, either
AI [DI is inconsistent, or for every A 2 N (P ), A or -A is in AI [DI. In the latter case, P gm
does not contain any negative literals. Furthermore P gm has no facts since it can be further
reduced otherwise. Therefore the only stable model of P gm, which is also the unique minimal
model M(P gm), is that every ground atom occurring in P gm is false. If A 2 AI and A 62 DI
for some ground atom A, -A must be true either in DI or in M(P gm), which is inconsistent
with the assumption in AI that A is true. 2
2.4 Backward Propagation of Assumed Truth Values
According to the definition of stable models, the assumed truth values of ground atoms should
coincide with the derived truth values. The assume-and-reduce algorithm uses forward chaining
to propagate the assumed truth values of ground atoms. This propagation may derive the truth
values of more ground atoms so that there is no need to lay down a choice point for guessing
their truth values.
incorporates backward propagation of assumed truth values of ground atoms under certain
conditions. Unlike forward propagation, which computes the derived truth values of ground
atoms, backward propagation of assumptions may lead to more assumptions, thus reducing the
search space for stable models.
Example 2.4 One application of stable models is to provide a semantics for programs with
choice constructs [26]. Suppose that three students are taking the AI class.
take(sean, ai). take(irene, ai). take(chris, ai).
The following ground program chooses exactly one student taking the AI class:
choose(sean,ai) :-diff(sean,ai).
diff(sean,ai) :- choose(irene,ai).
diff(sean,ai) :- choose(chris,ai).
choose(irene,ai) :-diff(irene,ai).
diff(irene,ai) :- choose(sean, ai).
diff(irene,ai) :- choose(chris,ai).
choose(chris,ai) :-diff(chris,ai).
diff(chris,ai) :- choose(sean,ai).
diff(chris,ai) :- choose(irene,ai).
There are three ground negative literals in the program. Suppose that diff(sean,ai) is assumed to
be false. By backward propagation, we can infer that both choose(irene,ai) and choose(chris,ai)
must be assumed to be false too. All three assumptions can be used to simplify the program to
the following:
choose(sean,ai).
diff(irene,ai) :- choose(sean,ai).
diff(chris,ai) :- choose(sean,ai).
A reduction of the program derives that diff(irene,ai) and diff(chris,ai) are true. 2
Let P be a finite ground program. SLG supports backward propagation under two situations:
ffl If a ground atom A is assumed to be true, and P contains exactly one clause with A in the
head, of the form
A :-
then every L i (1 - i - n) is assumed to be true;
ffl If a ground atom A is assumed to be false, then for every clause in P with A in the head
and a single literal L in the body, L is assumed to be false.
The backward propagation may be repeated several times. The correctness of backward propagation
is obvious according to the definition of stable models. The assume-and-reduce algorithm
can be modified to include backward propagation, the details of which are omitted.
3 Integration with Computation of the Well-Founded
The assume-and-reduce algorithm deals with only finite ground programs and computes (two-
valued) stable models. This section shows how to integrate computations of the well-founded
semantics and stable models to provide query evaluation of non-ground programs for practical
applications.
It is known that for logic programs without loops through negation, e.g., modularly stratified
programs [25], the well-founded partial model is total and coincides with the unique stable
model of the program. In that case, computation of the well-founded semantics is sufficient.
For programs with literals involved in loops through negation, the well-founded partial model
is in general three-valued. We discuss how negative loops should be handled in order to facilitate
computation of stable models and to ensure the polynomial time data complexity of query
evaluation under the well-founded semantics at the same time.
3.1 Handling Negative Loops
Negative loops occur due to recursion through negation. There are two main issues, namely how
to detect negative loops and how to treat literals that are involved in negative loops so that
query evaluation can proceed.
Example 3.1 Consider the following program [31]:
move(a,b). move(b,a). move(b,c). move(c,d).

Figure

2 shows a portion of the SLDNF tree for the query win(a), which contains an infinite
branch through negation. 2
?- win(a).
?- move(a,X), ~win(X).
?- ~win(b).
?- win(b).
?- move(b,Y), ~win(Y).
?- ~win(a). ?- ~win(c).
?- win(a). fail

Figure

2: SLDNF tree for win(a)
A simple mechanism for negative loop detection is to associate with each call a negative
context. This approach has been adopted in Well! [2] and in XOLDTNF resolution [6]. Consider
a branch through negation in an SLDNF tree. The negative context of a call on the branch
is the set of ground negative literals encountered along the path from the root to the call. In

Figure

2, the initial call win(a) has an empty negative context. The negative context for win(b)
is f-win(b)g, and the negative context for the second call of win(a) is f-win(b); -win(a)g.
In the tree for the second call win(a), when -win(b) is selected, it is in the negative context
of win(a), indicating that there is a negative loop. The approach in XOLDTNF resolution [6] is
to treat the selected ground negative literal -win(b) as undefined. In general, an answer consists
of not only an instance of a query atom, but also a truth value indicating whether the answer
is true or undefined. Figure 3 shows a portion of the XOLDTNF forest for query win(a). Each
node is labeled by a pseudo-clause. The head captures bindings of relevant variables that have
been accumulated and the truth value, and the body contains literals that are yet to be solved.
call: ({~win(b),~win(c)}, win(c))
(win(c),t) :- win(c).
(win(c),t) :- move(c,Z), ~win(Z).
(win(c),t) :- ~win(d).
(win(c),t).
(win(a),t) :- win(a).
(win(a),t) :- move(a,X), ~win(X).
call: ({}, win(a))
(win(a),t) :- ~win(b).
(win(b),t) :- win(b).
(win(b),t) :- move(b,Y), ~win(Y).
call: ({~win(b)}, win(b))
(win(b),t) :- ~win(a).
(win(a),u).
(win(b),t) :- ~win(c).
fail
(win(b),u).
call: ({~win(b),~win(a)}, win(a))
(win(a),t) :- win(a).
(win(a),t) :- move(a,X), ~win(X).
(win(a),t) :- ~win(b).
(win(a),u)

Figure

3: XOLDTNF forest for win(a)
The detection of negative loops using negative contexts is easy to implement in goal-oriented
query evaluation. However, associating with each call a negative context prevents the full sharing
of answers of a call across different negative contexts. Examples can be constructed in which a
subgoal may be evaluated in an exponential number of negative contexts [7], even though the
well-founded semantics is known to have a polynomial time data complexity.
Treating negative literals involved in negative loops as undefined is appropriate for query
evaluation under the well-founded semantics. But it destroys the mutual dependencies among
the negative literals. If a query turns out to be undefined in the well-founded semantics, there
is little information that can be used for computation of stable models.
In [7], we developed a framework called SLG resolution. It detects potential negative loops
by maintaining dependency information among calls incrementally. Each call (up to renaming
of variable) is evaluated at most once, allowing the full sharing of answers. When a potential
negative loop is detected, negative literals that are involved are delayed so that other literals in
the body of a clause can be evaluated. These delayed literals may be simplified later if they
become known to be true or false, or they may be returned as part of a conditional answer
otherwise.

Figure

4 shows a portion of the SLG forest for query win(a). A vertical bar (j) separates
delayed literals on the left and the remaining literals on the right in the body of a clause. Notice
win(a) :- win(a).
win(a) :- move(a,X), ~win(X).
win(a) :- ~win(b).
win(a) :- ~win(b) | .
fail

Figure

4: SLG forest for win(a)
that there is a conditional answer for win(a), namely win(a) :-win(b), and similarly for
win(b), win(b) :-win(a). These conditional answers constitute a residual program, to which
the assume-and-reduce algorithm can be applied to derive stable models and the answers of the
original query in each stable model.
3.2 Simplification of Delayed Literals
Given an arbitrary but fixed computation rule, there are programs in which ground negative
literals must be delayed before their truth or falsity is known.
Example 3.2 Assume that a left-most computation rule is used and that s is to be solved with
respect to the following program:
s :-p, -q, -r.
q :-s, -p, r.
r :-s, -q, p.
The first negative loop involves s and p, which is processed by delaying -p and -s. In the clause
of s, the next body literal -q is then selected, which leads to the second negative loop involving
s and q. Delaying is applied again so that query evaluation can proceed. The computation rule
selects the next body literal, namely -r, in the clause of s, whose evaluation results in the third
negative loop involving s and r. The literal -r in the clause of s and the literal -s in the clause
of r are delayed. At this point, the clause of s does not have any body literals that are not
delayed. Thus we derive a conditional answer for s, namely s :-p, -q, -r. The evaluation of p,
q, and r continues, leading to a negative loop involving p, q, and r. The corresponding negative
literals are delayed. Computation continues, and a positive loop is detected among p, q, and r.
They become completely evaluated without any answers, and so they are false. The falsity of p,
q, and r is then propagated to derive a true answer for s. 2
To facilitate the simplification of delayed literals, SLG sets up forward chaining links among
calls when a conditional answer is derived. When the truth value of a ground atom A becomes
known, all conditional answers with delayed literals A or -A are simplified.
Not all delayed literals can be simplified as the well-founded semantics is in general three-
valued. If a query has undefined instances under the well-founded semantics, its evaluation
produces a residual program consisting of all relevant conditional answers, as well as forward
chaining links for simplification of delayed literals.
For the program and query win(a) in Example 3.1, Figure 5 shows the residual program for
win(a) that consists of two conditional answers and the corresponding forward chaining links. A
link from win(b) to win(a) indicates that if win(b) is true or false, some conditional answer of
win(a) can be simplified. These forward chaining links are used directly in SLG for computation
of stable models, for propagation of assumed truth values of ground atoms and for reduction of
the residual program.

Figure

5: Residual program and forward chaining links for win(a)
3.3 General Logic Programs
Van Gelder has generalized the well-founded semantics of normal logic programs to the alternating
fixpoint logic of general logic programs [30]. The SLG resolution developed in [7] has been
extended for goal-oriented query evaluation of general logic programs [4]. Similarly it produces
a residual program and corresponding forward chaining links for queries that have undefined
instances under the alternating fixpoint logic.
Example 3.3 The following program describes a coloring of nodes in a graph in such a way
that two adjacent nodes cannot be both colored.
edge(a,b). edge(b,a). edge(b,c). edge(c,d).
Consider the query color(a). By By resolving (color(a) :- color(a)) with the program clause, we
obtain a new clause for color(a):
The literal, -edge(a,Y), is selected. The corresponding positive subgoal, edge(a,Y), is evaluated
completely and has one answer, namely edge(a,b). Hence -edge(a,Y) is true for all Y that is
distinct from b. We return the answer of edge(a,Y) to the clause for color(a). By resolving the
universal disjunction
8 Y. (-edge(a,Y) -color(Y))
with the answer edge(a,b), we derive a unit clause, color(b). The clause for color(a) is replaced
by the following clause:
color(a) :-color(b).
The literal, -color(b), is then selected. A new subgoal, color(b), is created and evaluated. Figure
6 shows the SLG forest resulted from the evaluation of color(a), where 8 is represented by All
and disjunction - is represented by ';'. Notice that color(d) is derived to be true and color(c)
is derived to be false, while both color(a) and color(b) are undefined. The residual program
consisting of
color(a) :-color(b).
can be further processed for stable model computation. 2
color(a) :- ~color(b) | .
color(c) :- color(c).
color(c) :- all(Y).(~edge(c,Y); ~color(Y)).
color(c) :- ~color(d).
fail
color(d) :- color(d).
color(d) :- all(Y).(~edge(d,Y); ~color(Y)).

Figure

forest for color(a)
3.4 Stable Models: Two-Valued versus Three-Valued
Let P be a program and Q be a query. SLG first evaluates Q with respect to the well-founded
semantics of P . The result includes a set of true and false instances of Q, and in general,
a residual program P und(Q) for undefined instances of Q. (Two-valued) stable models for the
residual program, P und(Q) , can be derived by using the assume-and-reduce algorithm. However, a
(two-valued) stable model of P und(Q) may or may not be extended to a (two-valued) stable model
of P .
Example 3.4 Consider the following simple program
a :-b.
b :-a.
and query b. The residual program for b contains two clauses:
b :-a.
a :-b.
There are two stable models for the residual program, one in which b is true and the other in
which a is true. However, the one in which b is true cannot be extended to a stable model of
the original program, even though there is a three-valued stable model of the original program
in which b is true. 2
In general, answers of a query computed by SLG are answers with respect to three-valued
stable models of a given program P . SLG does not enumerate all possible three-valued stable
models of P .
To compute (two-valued) stable models of a program P in SLG, one may define a new
predicate that calls all predicates in P with distinct variables as arguments. By evaluating the
new predicate (with distinct variables as arguments), SLG derives a residual program P und for
all undefined atoms of the original program. All (two-valued) stable models of P can be derived
by applying the assume-and-reduce algorithm to P und .
4 Integration with Prolog
All normal logic programs are obviously syntactically correct Prolog programs, even though
their execution under Prolog's strategy may not terminate. One of the objectives of the SLG
system is to integrate query evaluation with ordinary Prolog execution so that existing Prolog
environments can be readily used for knowledge-based applications. This section describes the
interface of SLG from a user's point of view.
4.1 Syntax
The syntax of Prolog is used for input programs, with additional directives for predicate declara-
tions. Predicates can be declared as tabled or prolog. Tabled predicates are evaluated using SLG
resolution. Prolog predicates are solved by calling Prolog directly. Calls to tabled predicates are
remembered in a table with their corresponding answers. Future calls to tabled predicates that
are renaming variants of previous calls are not re-evaluated, but will be satisfied using answers
that are computed as a result of the previous calls.
It is actually legal for a tabled predicate to call a Prolog predicate which in turn calls a tabled
predicate. However, the two invocations of tabled predicates will not share the same table, and
Prolog's infinite loops will not be terminated.
There are also certain constraints on the form of clauses that can be used to define tabled
predicates. In particular, the body of a clause for a tabled predicate should be a conjunction of
literals. Cuts are allowed in the body before any occurrence of a tabled predicate. Common uses
of cuts for selection of clauses according to certain guard conditions are supported for tabled
predicates.
Clauses with a universal disjunction of literals in the body are allowed. They are indicated
by an operator /\Gamma. For the program in Example 3.3, it will be written as follows:
where all variables that occur only in the body are universally quantified in the body, and
disjunction is indicated by ';'. Standard safety conditions are assumed [32]. To determine if
the body of a clause is safe to evaluate, we convert the universal quantification into existential
quantification:
The notion of safety requires that all free variables in the body must be bound when the negation
in the body is evaluated. For the conjunction inside the existential quantification, all variables
in a negative literal must also occur in the a positive literal. Accordingly we require that for a
clause with a universal disjunction of literals in the body, the head must be ground when the
clause is used, and all variables that occur in positive literals in the body also occur in the head
or in negative literals in the body.
4.2 Query Interface
Tabled predicates are evaluated with respect to the well-founded semantics by default. Both true
and conditional answers can be returned.
Example 4.1 The following is the winning program in Prolog syntax with a tabling directive
of SLG:
tabled win/1.
move(a,a). move(a,b). move(b,a). move(b,c).
By the initial default, all predicates are Prolog predicates unless declared otherwise. The default
can be changed to tabled by users if needed. The Prolog interface is also used for queries. In the
following, the first query asks for true answers under the well-founded semantics, and the second
returns also conditional answers, where each condition is a list of delayed literals.
no
noBy applying the assume-and-reduce algorithm to the residual program produced by the computation
of the well-founded semantics, SLG derives answers of queries under (two-valued) stable
models of the residual program (or three-valued stable models of the original program). (See
Section 3.4 for more discussions.) In general, there may be multiple stable models of the residual
program, and answers of queries have to be qualified by the corresponding stable model. SLG
provides a versatile interface for query evaluation under stable models of the residual program.
It includes the following predicates:
ffl st(Call,PSM) (or stnot(Call,PSM)): It succeeds if Call is a ground atom and there is a
stable model PSM in which Call is true (or false);
ffl stall(Call,Anss,PSM): It computes a stable model PSM and collects all answers of Call
in a list Anss.
ffl stselect(Call,PSM0,Anss,PSM): It is similar to stall/3, except that it computes only
those stable models in which all ground literals in PSM0 are true. This allows the user to
select only those stable models that satisfy certain conditions.
Alternative stable models of the residual program and the corresponding answers of Call are
returned upon backtracking.
Example 4.2 The following is a program that selects exactly one student for each course [26]:
tabled choose/2, diff/2.
take(sean,ai). take(irene,ai). take(chris,ai).
take(brad,db). take(irene,db). take(jenny,db).
same(X,X).
The query below selects those stable models in which choose(sean,ai)and "+choose(irene,db)
are true:
stselect(choose(-),[choose(sean,ai),"+choose(irene,db)],Anss,PSM).
no5 Related Work and Experimental Results
SLG seems to be the first work that provides integrated query evaluation under various semantics,
including the well-founded semantics and stable models of normal logic program, the alternating
fixpoint logic of general logic programs, and SLDNF resolution in Prolog execution. The combination
of Prolog's programming environment and SLG's query processing capabilities makes it
easier to develop knowledge-based applications.
The delaying mechanism for handling negative loops in SLG has two important implications.
First, it avoids redundant derivations in the computation of the well-founded semantics as delayed
literals are simplified away as needed using forward chaining links. Second, it allows SLG to
produce a residual program for undefined instances of a query, which can be used directly for
stable model computation. Most of existing techniques for query evaluation under the well-founded
semantics replace looping negative literals with an undefined truth value [2, 3, 6], or use
the alternating fixpoint method to compute possibly true or false facts [28]. In either case, little
information is saved for later computation of stable models.
Goal-oriented query evaluation with respect to stable models was studied by Dung in an
abductive framework [9]. It is a refinement of Eshghi and Kowalski's abductive procedure [11].
A ground negative literal can be assumed to be true if it does not lead to any inconsistency. It
is not clear how to specialize the abductive procedure to compute only answers that are valid in
the well-founded semantics. Pereira et al. [19] developed derivation procedures for goal-oriented
evaluation of ground programs under the well-founded semantics or stable models.
A bottom-up procedure, called backtracking fixpoint, was developed by Sacca and Zaniolo [26],
which non-deterministically constructs a stable model if one exists. In [15], stable models are
characterized by a transformation of normal logic programs into semantically equivalent positive
disjunctive programs, with integrity constraints in the denial form / each atom B,
is a new atom for the negation of B. Stable models are constructed using the model
generation theorem prover (MGTP), which is a bottom-up forward chaining system. Starting with
the set containing the empty interpretation, MGTP either expands an interpretation according to
a disjunctive clause or discards an interpretation if it violates some integrity constraints. Other
methods that construct all stable models simultaneously include [10, 20, 29].
The work most closely related to ours is the branch-and-bound method by Subrahmanian
et al. [29]. Their approach first computes Fitting's Kripke-Kleene semantics and at the same
time "compacts" the program by deleting parts of the program. The program is then processed
and further compacted by an alternating fixpoint procedure that computes the well-founded
semantics. The resulting program is used for computation of stable models using a branch-and-
bound method.
The branch-and-bound method and SLG are similar in the sense that both assume the truth
values of some atoms and compact or simplify the program as computation proceeds. However,
there are several major differences. First, the branch-and-bound method in [29] computes and
stores all stable models simultaneously. As the number of stable models can be exponential,
storing all stable models at the same time may require a substantial amount of memory. SLG,
on the other hand, computes alternative stable models through backtracking. Second, the branch-
and-bound method interleaves the assumption of the truth value of an atom with the computation
of the well-founded semantics. After the truth value of an atom is assumed, the resulting program
is processed with respect to the well-founded semantics. SLG only attempts to reduce the
program in such a way that ground atoms that are true or false in Clark's completion are
derived, which is simpler than a full-fledged computation of the well-founded semantics. Third,
the branch-and-bound method is intelligent in choosing which atom to make an assumption
about its truth value. It selects an atom in a leaf strongly connected component according
to the dependency graph. SLG uses a very simple criterion, namely only those atoms whose
complements occur in a program can be assumed. Finally, SLG integrates query evaluation with
ordinary Prolog execution and accepts programs with variables, while the method in [29] assumes
a finite ground program.
To get a rough idea how SLG performs, we took two benchmark programs reported in [29]
together with their timing information, and ran them using SLG. It should be pointed out that
a systematic study of benchmark programs have to be conducted before a clear picture of the
relative performance of the various systems can be obtained. The prototype compiler in [29]
was written in C running under the Unix environment on a Decstation 2100. SLG was written
in Prolog running under SICStus Prolog in the Unix environment on a Decstation 2100. The
timing information of SLG was obtained by Prolog builtin predicate statistics. All timing data
are in milliseconds.
The first program consists of the following rules:
An additional unary predicate y( ) is used to introduce constants in the program. To test the
program in SLG, we added the following rules:
The query m(X) is then evaluated by calling stall(m(X),Anss,PSM). A failure loop is used to
get all answers of the call. Table 7 shows the timing of SLG and the intelligent branch-and-bound
in [29]. The relative rate of increase in execution time in SLG seems closer to the rate of increase
of the number of stable models. The execution time of SLG falls below that of the intelligent
Number of constants 1 2 3 4 5
Number of stable models 4
Branch and bound 43 262 1413 9431 95766

Figure

7: SLG and branch-and-bound for enumerating all stable models
branch and bound when the number of constants reaches 5, probably due to the large number
of stable models that have to be stored in the latter.
The second program, also taken from [29], is as follows:
It is augmented by a unary predicate y( ) whose sole purpose is to introduce constant symbols
into the program. For SLG, we added y(X) at the beginning of the body of each rule for s(X).
The query s(X) is then evaluated by calling stall(s(X),Anss,PSM), and a failure loop is used
to check all possibilities. Table 8 shows the timing information of SLG versus the intelligent
branch and bound in [29]. In this case, there is no stable model for the program, which can be
detected as soon as the truth value of p(X), q(X), or r(X) for some X is assumed. Thus most of
the time is spent on the computation of the well-founded semantics.
Number of
Branch and bound 54 117 198 303 431 586 755 972 1203 1475

Figure

8: SLG and branch-and-bound for checking non-existence of stable models
The notion of stable models provides a declarative semantics for the choice construct in LDL
[18]. It has been shown by Greco et al. [14] that for certain classes of programs with choice,
the data complexity for computing a stable model is polynomial time. The choice construct has
been used to model a variety of applications where only one stable model is needed [14].
We tested SLG on a classical choice program [14]:
choose(X,Y) :- base(X,Y), choice(X,Y).
It is translated into a normal logic program:
choose(X,Y) :- base(X,Y), -diffchoice(X,Y).
diffchoice(X,Y) :- choose(X,Z), -same(Y,Z).
same(X,X).
The base relation contains a set of facts of the form:
base(i,a). base(i, b). base(i, c). base(i, d).
where i ranges from 1 to N, and N is used as a parameter. The query choose(X; Y ) is evaluated
by calling stall(choose(X,Y),Anss,PSM). We measured the time (on a Decstation 2100) for
computing the first solution for programs of different sizes by varying N from 2 to 10. Table 9
shows the timing of SLG for different values of N. The execution time of SLG seems polynomial
in the size of the base relation.

Figure

9: SLG for computing the first stable model
SLG is currently implemented as a Prolog meta interpreter [8], and therefore carries significant
overhead. A compiler implementation of SLG by extending the Warren Abstract Machine is being
carried out in the XSB project led by the second author [27]. XSB currently handles modularly
stratified programs. A preliminary performance analysis shows that XSB is over an order of
magnitude faster than SLG [5].
6 Conclusion
We have presented an assume-and-reduce algorithm for computing stable models and its integration
in SLG with goal-oriented query evaluation under the well-founded semantics, or more
generally the alternating fixpoint logic of general logic programs. The synergism exemplified
by SLG between Prolog on the one hand and deductive query processing and nonmonotonic
reasoning on the other offers an ideal environment for developing knowledge-based applications.



--R

Contributions to the theory of logic programming.

Tabulated resolution for well founded semantics.
Query evaluation of alternating fixpoint logic.
Efficient top-down computation of queries under the well-founded semantics

Query evaluation under the well founded semantics.
The SLG System
Negation as hypotheses: An abductive foundation for logic programming.
Computing stable models by using the ATMS.
Abduction compared with negation by failure.
On stratified autoepistemic theories.
The stable model semantics for logic programming.
Greedy by choice.
Transforming abductive logic programs to disjunctive programs.
Foundations of Logic Programming.
Autoepistemic logic.
A Logical Language for Data and Knowledge Bases.
Derivation procedures for extended stable models.
A truth maintenance system based on stable models.
Every logic program has a natural stratification and an iterated least fixed point model.
The well-founded semantics coincides with the three-valued stable se- mantics
Controlling the search in bottom-up evaluation
A procedural semantics for well-founded negation in logic programs
The Semantics of Deductive Databases.
Stable models and non-determinism for logic programs with nega- tion
The XSB Programmers Manual


The alternating fixpoint of logic programs with negation.
The well-founded semantics for general logic programs
Safety and translation of relational calculus queries.
--TR

--CTR
Chris Giannella , John Schlipf, An empirical study of the 4-valued Kripke-Kleene and 4-valued well-founded semantics in random propositional logic programs, Annals of Mathematics and Artificial Intelligence, v.25 n.3-4, p.275-309, 1999
Patrik Simons , Ilkka Niemel , Timo Soininen, Extending and implementing the stable model semantics, Artificial Intelligence, v.138 n.1-2, p.181-234, June 2002
Ilkka Niemel, Logic programs with stable model semantics as a constraint  programming paradigm, Annals of Mathematics and Artificial Intelligence, v.25 n.3-4, p.241-273, 1999
Thomas Eiter , Wolfgang Faber , Nicola Leone , Gerald Pfeifer, Declarative problem-solving using the DLV system, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
P. A. Bonatti, Resolution for Skeptical Stable Model Semantics, Journal of Automated Reasoning, v.27 n.4, p.391-421, November 2001
Francesco Calimeri , Wolfgang Faber , Gerald Pfeifer , Nicola Leone, Pruning Operators for Disjunctive Logic Programming Systems, Fundamenta Informaticae, v.71 n.2,3, p.183-214, August 2006
Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996
Francesco Calimeri , Giovambattista Ianni, Template programs for Disjunctive Logic Programming: An operational semantics, AI Communications, v.19 n.3, p.193-206, August 2006
Marcello Balduccini , Enrico Pontelli , Omar Elkhatib , Hung Le, Issues in parallel execution of non-monotonic reasoning systems, Parallel Computing, v.31 n.6, p.608-647, June 2005
Franois Bry , Adnan Yahya, Positive Unit Hyperresolution Tableaux and Their Application to Minimal Model Generation, Journal of Automated Reasoning, v.25 n.1, p.35-82, July 2000
V. s. Subrahmanian, Nonmonotonic Logic Programming, IEEE Transactions on Knowledge and Data Engineering, v.11 n.1, p.143-152, January 1999
Nicola Leone , Gerald Pfeifer , Wolfgang Faber , Thomas Eiter , Georg Gottlob , Simona Perri , Francesco Scarcello, The DLV system for knowledge representation and reasoning, ACM Transactions on Computational Logic (TOCL), v.7 n.3, p.499-562, July 2006
Jrgen Dix , Ulrich Furbach , Ilkka Niemel, Nonmonotonic reasoning: towards efficient calculi and implementations, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
stable model semantics;alternating fixpoint logic;deductive database;logic programming;logical query evaluation;nonmonotonic reasoning;well-founded semantics