Practical Methods for Proving Termination of General Logic Programs

E. Marchiori

Volume 4, 1996

Links to Full Text:

Abstract:
Termination of logic programs with negated body atoms (here called general logic programs) is an important topic. One reason is that many computational mechanisms used to process negated atoms, like Clark's negation as failure and Chan's constructive negation, are based on termination conditions. This paper introduces a methodology for proving termination of general logic programs w.r.t. the Prolog selection rule. The idea is to distinguish parts of the program depending on whether or not their termination depends on the selection rule. To this end, the notions of low-, weakly up-, and up-acceptable program are introduced. We use these notions to develop a methodology for proving termination of general logic programs, and show how interesting problems in non-monotonic reasoning can be formalized and implemented by means of terminating general logic programs.

Extracted Text

Journal of Artificial Intelligence Research 4 {1996} 179-208 Submitted 11/95;
published 4/96
 Practical Methods for Proving Termination of
 General Logic Programs Elena Marchiori elena@cwi.nl Centrum voor Wiskunde
en Informatica {CWI}
 P.O. Box 94079, 1090 GB Amsterdam, The Netherlands
 Abstract
 Termination of logic programs with negated body atoms {here called general
logic programs}is an important topic. One reason is that many computational
mechanisms
 used to process negated atoms, like Clark's negation as failure and Chan's
constructive
 negation, are based on termination conditions. This paper introduces a methodology
for
 proving termination of general logic programs w.r.t. the Prologselection
rule. The idea is to
 distinguish parts of the program depending on whether or not their termination
depends on
 the selection rule. To this end, the notions of low-, weakly up-, and up-acceptable
program
 are introduced. We use these notions to develop a methodology for proving
termination
 ofgeneral logic programs, and show how interesting problems in non-monotonic
reasoning can be formalized and implemented by means of terminating general
logic programs. 1. Introduction
 General logic programs {glp's for short} provide formalizations and implementations
for special forms of non-monotonicreasoning, as illustrated by Apt and Bol
{1994} and Baral and Gelfond {1994}. For example, Prolog's negation as finite
failure operator can be used
 to implement the temporal persistence problem in Artificial Intelligence
as a logic program
 {Kowalski & Sergot, 1986; Evans, 1990; Apt & Bezem, 1991}. The implementationof
 operators like Clark's negation as failure {Clark, 1978} and Chan's constructive
negation {Chan, 1988}, isbased on termination conditions. Therefore the study
of termination of glp's{e.g., De Schreye & Decorte, 1994} isan important
topic.
 Two classes of glp's that behave well w.r.t. termination are the so-called
acyclic and
 acceptable programs{Apt & Bezem, 1991; Apt & Pedreschi, 1991}. In fact,
Apt and Bezem
 {1991} prove that if negation as finite failure is incorporated into the
proof theory, then
 for any acyclic program, all sld-derivations with arbitrary selection rule
of ground queries
 terminate. The converse of this result, i.e., if a program terminates for
all ground queries, then it is acyclic, holds only under the assumption that
the program is `non-floundering'.
 Apt and Pedreschi {1991} establishanalogous results on termination for so-called
acceptable
 programs, this time w.r.t. the Prolog selection rule, which selects the
leftmost literal of a
 query.
 Floundering is an abnormal form of terminationwhich arises as soon as a
non-ground
 negated atom is selected, as explained e.g., in {Apt & Bol, 1994}. To treat
also non-ground negated atoms, Chan {1988} introduced a procedure known as
Chan's constructive negation.
 Using Chan's constructive negation, Marchiori {1996} showed that the notions
of acyclicity
 and acceptability provide a complete characterization of programs that terminate
for all
 ground queries.
 c
 fl1996 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved.Marchiori
 The notion of acceptability combines the definition of acyclicity with a
semantic condi- tion, and therefore proving acceptability may be rather cumbersome.
The aim of this paper
 is to develop a methodology for proving termination with respect to the
Prolog selection
 rule, by using as little semantic information as possible. A program P is
split into two parts, say P
 1
 and P
 2
 ; then one part is proven to be acyclic, the other one to be acceptable,
 and these results are combined to conclude that the original program is
terminating w.r.t.
 the Prolog selection rule. The decomposition of P is done in such a way
that no relations definedin P
 1
 occur in P
 2
 . We introduce the notions of up-acc eptability, where P 1
 is proven
 to be acceptable and P
 2
 to be acyclic, and of low-acc eptability, which treats the converse
 case {P
 1
 acyclic and P 2
 acceptable}. In order to be of more practical use, the notion of up-acceptability
is generalized to weak up-acc eptability . We integrate these notions in
a bottom-up methodology for proving termination of general logic programs.
We apply our
 results to programs formalizing problems in non-monotonic reasoning. In
particular, we
 show that the planning in the blocks world problem can be formalized and
implemented by
 means of an up-acceptable program. This provides a class of queries {up-bounded
queries}
 that can be completely answered.
 Even though our main theorems {Theorem 5.5, 6.4 and 7.2} deal with Chan's
construc- tive negation only, a simple inspection of the proofs shows that
they hold equally well for
 the case of negation as finite failure.
 Our approach provides a simple methodology for proving termination of glp's,
by com-
 bining the results of Bezem, Apt and Pedreschi on acyclic and acceptable
programs. The
 relevance of this methodology is twofold: for a large class of programs,
it overcomes the
 drawback of the method of Apt and Pedreschi {1991}, namely the use of too
much semantic
 information; and it allows to identify those parts of the program whose
termination is de-
 pendent on the use of the Prolog selection rule. Moreover, theexamples that
are given, show
 that systems based on the logic programming paradigm provide a suitable
formalization and implementation for problems in non-monotonic reasoning.
 The paper is organized as follows. The next section contains some terminology
and
 preliminaries.In Sections 3 and 4 the notions of acyclicity and acceptability
are presented.
 Sections 5, 6, and 7, contain our alternative definitionsof acceptability.
In Section 8 these
 definitions are integrated in a methodology for proving termination. Finally,
in Section 9 some conclusions are given. This paper is an extended and revised
version of {Marchiori,
 1995}.
 2. Preliminaries
 The following notation will be used. We follow Prolog syntax and assume
that a string
 starting with a capital letter represents a variable, while other strings
represent constants, terms and relations. Relation symbols are often denoted
by p; q; r. A literal is either an
 atom p{s
 1
 ; : : : ; s
 k
 }, or a negated atom :p{s 1
 ; : : : ; s k
 }, or an equality s = t, or an inequality 8{s 6= t}, where 8 quantifies
over some {perhaps none} of the variables occurring in s, t.
 Equalities and inequalities are also called constr aints, and denoted by
c. An inequality 8{s 6= t} is primitive if it is satisfiable but not valid.
For instance, X 6= a is primitive. An {extended} general logic pro gr am
, denoted by P , R, is a finite set of clauses
 H   L
 1
 ; : : : ; L
 m
 :
 180Proving Termination of General Logic Programs
 with m 025 0, where H is an atom, and L
 i is a literal, for i 2 [1; m]. A query is a finite
 sequence of literals, and is denoted by Q.
 To treat negated non-ground atoms, Chan {1988} proposesto augment sld-resolution
with a procedure, informally described as follows. For a substitution 022
= fX
 1
 =t 1
 ; : : : ; X n
 =t
 n
 g,
 we denote by E 022
 the equality formula {X
 1
 = t
 1
 ^ : : : ^ X n
 = t
 n }. For any negated atom :A,
 ifall the sld-derivations of A are finite, and 022
 1
 , : : : ; 022
 k
 , with k 0250, are the computed answer substitutions, then the answers
for :A are obtained from the negation of 9{E
 022
 1 _ : : : _ E
 022
 k
 },
 where 9 quantifies over the variables not occurring in A. For instance,
consider the program p{a}  .
 p{b}  .
 The answer to the query :p{X } is X 6= a ^ X 6= b. We call sldcnf-resolution,
sld-
 resolution augmented with Chan's procedure. To show the correctness of sldcnf-resolution,
 we choose as program semantics the Clark's completion {Clark, 1978}. This
semantics is a
 natural interpretation of a glp as a set of definitions. Intuitively, the
Clark's completion
 of a program P , denoted by comp{P }, is the first-order theory obtained
by replacing the
 implication of each clause of P with an equivalence. It is constructed as
follows. Below, 8
 quantifies over X 1
 ; : : : ; X k
 .
 
*  For every relation symbol p occurring in P , having say k 025 0 arguments:
 { if p does not occur in the head of any clause then add the formula 8{p{X
 1
 ; : : : ; X
 k
 } $ false }; { otherwise, if k =0 then add the formula p $ true ; if k >0
and C 1
 ; : : : ; C l
 , with
 l 025 1 are all the clauses of P with head symbol p, with C
 i
 =p{s
 i
 1
 ; : : : ; s
 i
 k }   Q
 i
 ,
 then add the formula 8{p{X
 1 ; : : : ; X
 k } $ _
 i2[1;l]
 {9V
 i
 {E
 i ^ Q
 i
 }), where V
 i
 is the set of variables of C i
 , E
 i is {s
 i
 1
 = X
 1
 ^ : : : ^ s
 i
 k
 = X k
 }, and X
 1
 ; : : : ; X
 k
 are fresh
 variables.
 
*  Finally, the following fre e equality axioms are added, so that the equality
theory of
 comp{P } becomes the same as the one of the Herbrand universe.
 { f {X
 1
 ; : : : ; X k
 } = f {Y
 1
 ; : : : ; Y k
 } ! {X 1
 = Y
 1 ^ : : : ^ X k
 = Y
 k },
 for every function symbol f ,
 { f {X
 1
 ; : : : ; X k
 } 6= g{Y
 1
 ; : : : ; Y
 m
 },
 for every distinctfunction symbols f and g,
 { X 6= s,
 for every terms s.t. X occurs in s.
 The soundness of sldcnf-resolution w.r.t. Clark's semantics follows from
comp{P } j= 8{A $ 9{E
 022
 1
 _ : : : _ E
 022
 k
 }); where 8 quantifies over all the free variables of the formula. sldcnf-resolution
is complete
 only for queries having all terminating derivation. In fact, Chan's procedure
is not defined
 if A has an infinite derivation. As a consequence, thenotion of {infinite}
derivation is
 181Marchiori
 not always defined. This is a problem for the study of termination of glp's,
because
 the notion of derivation is of crucial importance. Therefore, we refer here
to an alternative definition of Chan's procedure given by Marchiori {1996},
wherethe subtrees used to resolve
 negative literals are built in a top-down way, constructing their branches
in parallel. As a
 consequence, the mainderivation is infinite if at least one of these subtrees
is infinite.
 Termination of glp's depends on the selection rule. For instance, the program
p   q,p.
 terminates if the Prolog selection rule, whichchooses the leftmost literal
of a query, is
 used. But, the program does not terminate if the selection rule which chooses
the rightmost
 literal of a query is used. We shall consider the generalization of the
Prolog selection
 rule to programscontaining constraints, which delays the selection of primitive
constraints
 as follows: the leftmost literal of a query which is not a primitive inequality
is chosen.
 For simplicity, we continue to refer to this selection rule as the Prolo
g selection rule . An
 sldcnf-tree that is obtained by using the Prolog selection rule is called
ldcnf-tree.
 To prove terminationof logic programs, suitable functions from ground atoms
to natural
 numbers, called level mappings, will be used. Let B
 P
 denote the Herbrand base of P .
 Definition 2.1 {Level Mapping} A level mapping {for P } is a function j
j from B
 P
 to natural numbers. 2 A level mappingis extended to negated ground atoms
by j:Aj = jAj. We do not need to extend this notion also to constraints,
because they represent terminatingatomic actions. However, note that the
presence of constraints in a query influences termination, because,
 for instance, a derivation finitely fails if an unsatisfiable constraint
is selected.
 3. Acyclic Programs Our method will be based on the notions of acyclicity
and acceptability, which are used
 to characterize a class of terminating programs w.r.t. an arbitrary and
the Prolog selection
 rule, respectively. In this section we recall the definition of acyclicity,
and some useful results from {Marchiori, 1996}, while acceptability willbe
discussed in Section 4. Apt and Bezem {1991} study termination of glp's w.r.t.
an arbitrary selection rule. They introduce the following elegant syntactic
notion.
 Definition 3.1 {Acyclic Program} A program P is acyclic w.r.t. a level mapping
j j if
 for all ground instances H   L
 1
 ; : : : ; L
 n
 of clauses of P we have that jH j > jL
 i
 j holds for
 all i 024 1 024 n s.t. L
 i
 is not a constraint. P is acyclic if there exists a level mapping j j s.t.
 P is acyclic w.r.t. j j. 2 If a program is acyclic, then all ground queries
have only finite derivations, and hence
 terminate. To extend this result to non-ground queries, the following notion
of boundedness
 is used.
 Definition 3.2 {Bounded Query} Let jj be a level mapping. A query Q = L
 1 ; : : : ; L
 n is
 bounded {w.r.t. j j} if for every 1 024 i 024 n, the set
 jQj
 i
 = fjL
 0
 i j j L
 0
 i
 is a ground instance of L
 i
 g
 182Proving Termination of General Logic Programs
 is finite. 2
 Notice that ground queries are bounded. Apt and Bezem prove that for an
acyclic program, every bounded query Q has only finite derivations w.r.t.
negation as finite failure.
 Theconverse of this result does not hold, due to the possibility of floundering.
Instead, using
 Chan's constructive negation, we obtain a complete characterization {Marchiori,
1996}. First, we formalize the concept of termination w.r.t. an arbitrary
selection rule.
 Definition 3.3 {Terminating Query and Program} A query is terminating {w.r.t.
P } if
 all its sldcnf-derivations {in P } are finite. A program P is terminating
if all ground queries
 are terminatingw.r.t. P . 2
 Theorem 3.4 Let P be an acyclic pro gr am and let Q be a bounde d query.
Then every sldcnf-tre e for Q in P contains only bounde d queries and is
finite.
 Theorem 3.5 Let P be a terminating pro gr am. Then there exists a level
mapping j j s.t.:
 {i} P is acyclic w.r.t. j j; {ii} for every query Q, Q is bounde d w.r.t.
jj iff Q is terminating.
 From Theorems 3.4 and 3.5 it follows that terminating programs coincide
with acyclic
 programs and that for acyclic programs a query has a finite sldcnf-tree
if and only if it is bounded. Notice that when negation as finite failure
is assumed, Theorem 3.5 does not hold. For instance, the program: p{X}  
: q{Y}.
 q{s{X})   q{X}.
 q{0}  .
 is terminating {floundering} but it is not acyclic.
 Finding a level mappingfor proving acyclicity is a creative process. We
refer the reader to {De Schreye & Decorte, 1994}for a thorough presentation
of various techniques for
 constructing level mappings.
 The following section illustrates how an interesting problem in nonmonotonic
reasoning
 can be formalized and implementedas an acyclic program. 3.1 An Example:
Blocks World
 The blocks world is a formulation of a problem in AI, where a robot performs
a number
 of primitiveactions in a simple world {see for instance Nilsson, 1982}.
Here we consider asimpler version of this problem by Sacerdoti {1977}. There
are three blocks a, b, c, and
 three different positions p, q, r on a table. A block can lay either above
another block or on one of these positions, and it can be moved from one
position to another. The problem
 consists of specifying possible configurations, i.e., those obtained from
the initialsituation
 by performing a sequence of possible moves. An example of an initial situation
is given in
 Figure 1.
 Kowalski {1979} gives a clausal representation of this problem by means
of pre- and post-
 conditions. Here we formulate the problemusing McCarthy and Hayes' situationcalculus
 183Marchiori
cprqbaFigure 1: The Blocks-World
 {McCarthy & Hayes, 1969}, in terms of facts, events and situations. There
are three types of facts: loc{X; L} stands for `block X is in location L';
above {X; Y } for `block X is on
 block Y '; and clear {L} for `there is no block in location L'. There is
only one type of event:
 move {X; L} stands for `move block X into location L'. Finally, situations
are described
 usinglists: [ ] denotes the initial situation, and [X ejX s] the situation
obtained from X s
 by performing the event X e. Based on the above representation, the blocks
world can be formalized as the following glp blocksworld:
 1} holds{l,[]}   : l2 L
 2} block{bl}   : bl2 B
 3} position{pl}   : pl2 P
 4} holds{loc{X,L},[move{X,L}|Xs]}   block{X},
 position{L},
 holds{clear{top{X}),Xs},
 holds{clear{L},Xs},
 L 6= top{X}.
 5} holds{loc{X,L},[Xe|Xs]}   block{X},
 position{L},
 : abnormal{loc{X,L},Xe,Xs},
 holds{loc{X,L},Xs}.
 6} holds{above{X,Y},Xs}  
 holds{loc{X,top{Y}),Xs}.
 7} holds{above{X,Y},Xs}  
 holds{loc{X,top{Z}),Xs},
 holds{loc{Z,top{Y}),Xs}.
 8} holds{clear{L},Xs}  
 : occupied{L,Xs}.
 9} abnormal{loc{X,L},move{X,L'},Xs}  .
 184Proving Termination of General Logic Programs
 10} occupied{L,Xs} 
 holds{loc{X,L},Xs}.
 11} legals{[{a,L1},{b,L2},{c,L3}],Xs}  
 holds{loc{a,L1},Xs},
 holds{loc{b,L2},Xs},
 holds{loc{c,L3},Xs}. Here top{X} denotes the top of block X, B = fa; b;
cg, P = fp; q; r; top{a}; top{b}; top{c}g,
 and L = floc{a; p}; loc{b; q}; loc{c; r}g. Moreover, lines1, 2 and 3 abbreviate
sets of clauses, and line 1 specifies the initial situation. The relation
holds describes when a fact is possible
 in a given situation, and the relation legals when a configuration is possible
in a given
 situation. Consider the following level mapping, where for a ground term
y, jyj denotes the length
 of the list y, otherwise {i.e., if y isnot a list} jyj is 0.
 jblock{x}j = 0, jposition{x}j = 0,
 jabnormal{x; y; z}j = 0, jholds{x; y}j =
 8
 >
 >
 >
 <
 >
 > >
 :
 3 003 jyj + 1 if x is of the form loc {r; s}, 3 003 jyj + 3 if x is of
the form clear {r; s},
 3 003 jyj + 4 if x is of the form above {r; s},
 0 otherwise. joccupied{x; y}j = 3003 jyj + 2, jlegals{x; y}j = 3003 jyj
+ 2.
 It is easy to check that blocksworld is acyclic w.r.t. j j.
 Therefore, the class of questions expressed by means of boundedqueries can
be com-
 pletely answered. For instance, the question `when block a remainsin its
initial position p
 under the occurrence of an action?' can be formalized as the query holds{loc{a,p},[A]}.
 This query is bounded, hence every of its sldcnf-derivations is finite,
with answer 8L{A6=
 move{a; L}).
 Note that this query would flounder when negation as finite failure is used.
 4. Acceptable Programs
 In the previous section, we have seen how termination of glp's w.r.t. an
arbitrary selection
 rule can be proven by means of the notion of acyclicity. The notion of acceptability
{Apt
 & Pedreschi, 1991} is used for proving termination of glp's w.r.t. the Prolog
selection rule. In this section, we recall this notion, together with some
useful results from {Marchiori, 1996}. Acyclicity and acceptability will
be combined in the following sections to provide
 more practical tools for proving termination of glp's w.r.t. the Prolog
selection rule.
 In order to study terminationof general logic programs with respect to the
Prolog selection rule, Apt and Pedreschi {1991} introducedthe notion of acceptable
program. This
 185Marchiori
 notion is based on the same condition used to define acyclic programs, except
that, for a
 ground instance H   L
 1
 ; : : : ; L
 n
 of a clause, the test jH j > jL
 i
 j is performed only until the
 first literal Ln
 which fails. This is sufficient since, due to the Prolog selection rule,
literals
 after Ln
 will not be selected. To computen, a class of models of P , here called
spe cialize d
 mo dels, isused. The following notion is used. The restriction of an interpretation
I to a
 set S ofrelations, denoted by I
 jS
 , is the set of atoms of I having their relations in S . Definition 4.1
{Specialized Model} Let N eg
 P
 be the least set S of relations s.t.: the
 relations of P occurring in negated atoms are in S ; and if an element of
S occurs in the
 head of a clause, then all the relations occurring in the body of that clause
are in S . Let
 P 000
 be the set of clauses in P whose head contains a relation from N eg
 P
 . Now a modelI
 of P is spe cialize d if I jN eg
 P
 is a modelof comp{P 000
 }. 2
 Definition 4.2 {Acceptable Program} Let j j be a level mapping for P and
let I be an interpretation of P . P is acc eptable w.r.t. jj and I if I is
a specialized model of P , and
 forall ground instances H   L
 1
 ; : : : ; L
 n
 of clauses of P we have that jH j > jL
 i j holds for
 every 1024 i 024n s.t. L
 i
 is not a constraint, wheren = min{fng [ fi 2 [1; n] j I 6j= L
 i
 g}. P is
 acc eptable if it is acceptable w.r.t. some level mapping and interpretation.
2
 If a program is acceptable, then every ground query has only finite ldcnf-derivations,
 hence it terminates. To extend this result to non-ground queries, as for
the acyclic case,
 the following notion of boundedness is used.
 Definition 4.3 {Bounded Query} Let j j be a level mapping and let I be a
specialized
 model of P . A query Q = L
 1
 ; : : : ; L n
 is bounded {w.r.t. j j and I } if for every 1 024 i 024 n
 jQj
 i
 I
 = fjL
 0
 i j j L
 0
 1
 ; : : : ; L
 0
 i
 ground instance of L
 1
 ; : : : ; L i
 and
 I j= L
 0
 1
 ; : : : ; L
 0
 i0001
 g
 is finite. 2 Apt and Pedreschi prove that for an acceptable program, every
bounded query has only
 finite derivations w.r.t. the Prolog selection rule and negation as finite
failure. The converse
 of this result holds when Chan's constructive negation is used {Marchiori,
1996}. First, we
 formalize the concept of termination w.r.t. the Prolog selection rule.
 Definition 4.4 {Left-Terminating Query and Program} A query is left-terminating
 {w.r.t. P } if all its ldcnf-derivations are finite. A program P is left-terminating
if every
 ground query is left-terminating w.r.t. P . 2
 Theorem 4.5 Let P be an acc eptable pro gr am and let Q be a bounde d query.
Then every
 ldcnf-tre e for Q in P contains only bounde d queries and is finite. Theorem
4.6 Let P be a left-terminating pro gr am. Then there exists a level mapping
j j,
 and a spe cialize d model I of P s.t.: {i} P is acc eptable w.r.t. j j and
I ; {ii} for every query
 Q, Q is bounde d w.r.t. j j and I iff Q is left-terminating.
 In the following section an acceptable programthat formalizes planning in
the blocks world
 is given. 186Proving Termination of General Logic Programs
 4.1 An Example: Planning in the Blocks World
 Consider planning in the blocks world, amountingto the specification of
a sequence of
 possible moves transforming the initial configuration into a final configuration,
e.g., as
 in Figure 2. This problem can be solved using a nondeterministic algorithm
{Sterling & Shapiro, 1994}: while the desire d configur ation has not yet
be en re ache d, find a legal action,
 update the current configur ation, and check that it was not alre ady obtained.
The following
 program planning follows this approach: it consists of all the clauses of
the program blocksworld, minus 6} and 7}, and plus the following clauses:bacprqacbpqrFigure
2: Planning in the Blocks-World
 1p} transform{Xs,St,Plan}   state{St0},
 legals{St0,Xs}, trans{Xs,St,[St0],Plan}.
 2p} trans{Xs,St,Vis,[ ]}   legals{St,Xs}.
 3p} trans{Xs,St,Vis,[Act|Acts]}  
 state{St1},
 : member{St1,Vis}, legals{St1,[Act|Xs]},
 trans{[Act|Xs],St,[St1|Vis],Acts}.
 4p} state{[{a,L1},{b,L2},{c,L3}]}   P=[p,q,r,top{a},top{b},top{c}], member{L1,P},
 member{L2,P}, member{L3,P}.
 5p} member{X,[X|Y]}  .
 187Marchiori
 6p} member{X,[Y|Z]}   member{X,Z}.
 Planning in the blocks-world is specified by the relation transform: in
clause 1p} first a
 legal configuration for the actual situation is found by means of the predicate
legals; then
 the predicate trans is used to construct incrementallya plan from this configuration
to the final one. It uses an accumulator as third argument, to guarantee
that a plan does not
 pass twice through the same configuration. Clause 3p} takes care of expanding
a plan: it
 first looks for a configuration which was not already considered, and then
it adds to the plan the legal action yielding that configuration. Clause
2p} guarantees terminationof the
 construction when the final configuration is reached.
 To prove the acceptability of planning, we have to find a modelof planning
that is
 also a model of comp{f5p}; 6p}g[ blocksworldnf6}; 7}; 11}g}. We do not need
to use all this semantic information, because fromthe acyclicity of blocksworld,
it follows that
 planning is left-terminating if the following program tras is acceptable.
We postpone the
 justification of this claim till the next section.
 1
 0
 p} transform{Xs,St,Plan}  
 state{St0}, trans{Xs,St,[St0],Plan}.
 2p} trans{Xs,St,Vis,[ ]}  .
 3
 0
 p} trans{Xs,St,Vis,[Act|Acts]}   state{St1},
 : member{St1,Vis}, trans{[Act|Xs],St,[St1|Vis],Acts}. 4p} state{[{a,L1},{b,L2},{c,L3}]}
 P=[p,q,r,top{a},top{b},top{c}],
 member{L1,P},
 member{L2,P}, member{L3,P}.
 5p} member{X,[X|Y]}  .
 6p} member{X,[Y|Z]}   member{X,Z}.
 tras is obtained from planning by first deleting the subprogram `defining'
legals, and
 next the literals with relation legals occurring in the body of the remaining
clauses. By considering tras, we need less semantic information, namely a
modelof tras that is also a
 model of comp{f5p}; 6}g}. To show that tras is acceptable, we consider the
following level
 mapping:
 jmember{x; y}j = jyj;
 jstate{x}j = 7;
 jtrans{x; y; z; w}j = tot 000 card{el{z} \ S } + 3 003 {jxj + 1} + 5
+ jzj;
 188Proving Termination of General Logic Programs
 jtransf orm{x; y; z}j = tot + 3 003 {jxj + 1} + 6. Above, S denotes f[{a;
p1}; {b; p2}; {c; p3}] j fp1; p2; p3g 032 fp; q; r; top{a}; top{b}; top{c}gg,
and tot is the cardinality of S . Moreover, if z is a list then el{z} denotes
the set of its
 elements, otherwise it denotes the empty set; card{el{z} \ S } is the cardinality
of the set
 el{z} \ S ; finally, if x is a list then jxj denotes its length, otherwise
it denotes 0. Observe that
 {tot 000 card{el{z} \ S }) 025 0. Thus j j is well defined. For an atom
p{s
 1
 ; : : : ; s n
 }, we denote by [p{s
 1 ; : : : ; s
 n }] the set of all its ground instances. Consider the following interpretation
I = I
 transf orm
 [ I
 trans [ I
 member
 [ I
 state
 of tras, with:
 I
 transf orm
 = [transf orm{X; Y ; Z }], I
 trans
 = [trans{X; Y ; Z; W }],
 I
 member = fmember{x; y} j y is a list s.t. x 2 set{y}g,
 I
 state
 = fstate{x} j x 2 S g.
 It is easy to prove that I is a modelof tras. Moreover, N eg tras
 = fmemberg, and
 tras
 000 is equal to f5p}; 6p}g. So, I
 jfmemberg
 isa modelof comp{tras 000
 }. To show that tras is acceptable w.r.t. I and jj, we use the following
properties of j j, which are readily
 verified:
 jtransf orm{x; y; z}j 1
 025 8; {1}
 jtrans{x; y; z; w}j
 1 025 8; {2} jtrans{x; y; z; w}j
 1
 > jzj: {3}
 The proof of the acceptability of tras proceeds as follows:
 
*  Consider a ground instance:
 transf orm{xs; xt; plan}   state{st0}; trans{xs; st; [st0]; plan}:
 of 1p}. From {1} it follows that:
 jtransf orm{xs; xt; plan}j > jstate{st0}j:
 Suppose that I j= state{st0}. Then st0 2 S , so card{el{S \ el{[st0]})
= 1; hence: jtransf orm{xs; xt; plan}j > jtrans{xs; st; [st0]; plan}j:
 
*  Consider a ground instance:
 trans{xs; st; vis; [actjacts]}  
 state{st1}; :member{st1; vis}; trans{[actjxs]; st; [st1jvis]; acts}:
 of 2
 0
 p}. From {2} it follows that:
 jtrans{xs; st; vis; [actjacts]}j > jstate{st1}j; 189Marchiori
 and from {3}:
 jtrans{xs; st; vis; [actjacts]}j > j:member{st1; vis}j: Suppose that I j=
state{st1}; :member{st1; vis}. Then st1 2 S , but st1 62 set{vis}; so card{S
\ el{[st1jvis]}) = card{S\ el{vis}) + 1; hence tot 000 card{S \ el{[st1jvis]})
<
 tot 000 card{S \ el{vis}). Therefore,
 jtrans{xs; st; vis; [actjacts]}j > jtrans{[actjxs]; st; [st1jvis]; acts}j:
 
*  The proof for the other clauses of tras is similar.
 5. Up-Acceptability In this section, we introduce a first integration, called
up-acceptability, of the notions of
 acyclicity and acceptability. We show that up-acceptability provides a more
practical tool than acceptability for proving left-termination of glp's.
 In Section 4.1 we claimthat in order to prove left-terminationof planning,
it is sufficient
 to prove acceptability of the `part' of planning called tras and acyclicity
of the rest of the
 program. Let us explain how we arrive to this conclusion. First, planning
is partitioned
 into two parts: an upper part, say P 1
 consisting of clauses 1}; : : : ; 6}, and a lower part, say
 R, consisting of the rest of planning. This partition is such that no relation
defined in
 P
 1
 occurs in R. This kind of partitioning of a program is defined by Apt, Marchiori
and
 Palamidessi {1994} as follows. Say that a relation is defined in P if it
occurs in the head of at least one of its clauses, and that a literal is
defined in P if its relation is defined in P .
 Definition 5.1 {Program Extension} A program P extends a pro gr am R, denoted
by
 P > R, if no relation defined in P occurs in R. 2 So P extends R if P defines
new relations possibly using the relations defined already
 in R. For instance, the program P
 2
 :
 p   q,r.
 extends the program P
 1
 :
 q   s.
 s  .
 Next, we consider the program tras obtained from P
 1
 by deleting all the literals defined in R. We call this operation differenc
e, defined as follows.
 Definition 5.2 {Difference of Two Programs} The differenc e of the pro gr
ams P and R,
 denoted by P 011 R, is the program obtained from P by deleting all the
clauses of R and all
 the literals defined in R. 2
 190Proving Termination of General Logic Programs
 For instance, if P
 1 and P
 2
 are defined as above, then P
 2 011 P
 1
 is the program p  r.
 Finally, we prove that tras is acceptable and that R is acyclic, and in
doing that we
 have to take care that the two level mappingsused are related by a condition,
namely that
 for every ground instance, say C = H   Q
 1 ; L; Q
 2
 , of a clause of P
 1
 , for every literal L
 contained in C and defined in R, the level mapping of L is not greater than
the level mapping
 of H . This condition is important to ensure left-termination. For instance,
consider the program P
 1} q{f{X})  p{Y}, q{X}.
 2} p{f{X})  p{X}.
 and take P 1
 = f1}g and R = f2}g. Then P
 1
 extends R, P
 1
 011 R is acceptable w.r.t. the level mapping jq{x}j
 P
 1
 = jxj, R is acyclic w.r.t. the level mappingjp{x}j
 R
 = jxj, butP is not
 left-terminating.
 So, the steps we applied to planning are summarized in the following definition
of
 up-acceptability, that characterizes left-terminating programs.
 For a level mappingj j and a programR, the restriction of j j to R, denoted
j j
 jR , is the
 level mapping for R defined by jAj jR
 = jAj.
 Definition 5.3 {Up-Acceptability} Let j jbe a level mappingfor P . Let R
be s.t.
 P = P 1
 [ R for some P
 1
 , and let I be an interpretation of P 011 R. P is up-acc eptable w.r.t.
 j j, R and I if the following conditions hold:
 1. P
 1
 extends R;
 2. P 011 R is acceptable w.r.t. j j
 jP 011R
 and I ;
 3. R is acyclic w.r.t. j j jR
 ;
 4. for every ground instance H   L
 1
 ; : : : ; L n
 of a clause of P
 1
 , for every 1 024 i 024 n,
 
*  if L
 i
 is defined in R and is not a constraint, and 
*  if I j= L
 i1
 ; : : : ; L
 ik
 , where L i1
 ; : : : ; L ik
 are those literals among L
 1
 ; : : : ; L i
 whose
 relations occur in P 011 R, then jH j 025 jL
 i
 j.
 A program is up-acc eptable if there exist j j, R and I s.t. P is up-acceptable
w.r.t. j j, R, I . 2
 Observe that by taking for R the empty set of clauses, we obtain the original
definition
 of acceptability. Next, we introduce the notion of up-bounde d query.
 Definition 5.4 {Up-bounded Query} Let P be up-acceptable w.r.t. j j, R and
I , and let
 Q = L
 1
 ; : : : ; L
 n
 . Q is up-bounded if for every 1 024 i 024 n the set jQj
 up;I
 i
 = fjL
 0 i
 j j L
 0
 1
 ; : : : ; L 0
 n
 is a ground instance of Q and I j= L
 0
 k
 1
 ^ : : : ^ L
 0
 k
 l g
 is finite, where L
 0
 k
 1 ; : : : ; L
 0 k
 l
 are the literals of L
 0
 1
 ; : : : ; L
 0
 i0001
 whose relations occur in P 011 R.
 2 191Marchiori
 In order to show that all ldcnf-derivations of an up-bounded query are finite:
we shall
 prove that a ldcnf-derivation of an up-bounded query contains only up-bounded
queries;
 and we shall associate with each derivation of the query a descending chain
in the well-
 founded set of pairs of multisets of natural numbers, with the lexicographic
order. Recall
 that a multiset {see e.g., Deshowitz, 1987} is a unordered collection in
which the number of occurrences of each element is counted. Formally , a
multisetof natural numbersis a
 function from the set {N , <} of natural numbers to itself, giving the multiplicity
of each
 naturalnumber. Then, the ordering <
 mul on multisets is defined as the transitive closure
 of the replacement of a natural number with any finite number {possibly
zero} of natural
 numbers that are smallerunder <. Since < is well-founded, the induced ordering
<
 mul
 is
 also well-founded. For simplicity we shall omit in the sequel the subscript
mul from <
 mul
 .
 With an up-bounded query Q, we associate a pair 031{Q}
 up;I
 = {j[Q]j
 up;I ;P
 1
 ; j[Q]j
 up;I ;R
 } of
 multisets, where for a program P and an interpretation I
 j[Q]j up;I ;P
 = bag{maxjQj
 up;I k
 1
 ; : : : ; maxjQj
 up;I
 k m
 };
 where L
 k
 1
 ; : : : ; L
 k
 m are those literals of Q whose relations occur in P 011 R, and maxjQj
 up;I i
 is the maximum of jQj
 up;I
 i {which is by convention 0 if jQj
 up;I
 i is the empty set}.
 Recall that the lexicographic order 036 {on pairs of multisets} is defined
by {X; Y } 036
 {Z; W } iff either X < Z , or X = Z and Y < W .
 Then we can prove the following result.
 Theorem 5.5 Suppose that P is up-acc eptable w.r.t. jj, R and I . Let Q
be an up-bounde d
 query. Then every ldcnf-derivation for Q in P contains only up-bounde d
queries and is
 finite. Pro of. Let 030 = Q
 1
 ; : : : ; Q n
 ; : : : be a ldcnf-derivation for Q in P . We prove by induction on
 n that Q
 n is up-bounded, and that if it is the resolvent of a query Q
 n0001
 by the selection of a literal which is not a constraint, then 031{Q
 n
 } up;I
 < 031{Q n0001
 }
 up;I
 .
 For the base case n = 1, we have that Q
 1
 is up-bounded by assumption. Now consider
 n > 1, and suppose that the result holds for n 000 1. Thus, Q n0001
 is up-bounded. Suppose
 that the resolvent of Q
 n0001
 is defined and that the selected literal, say L, is not a constraint.
 It follows from the fact that Q
 n0001
 is up-bounded and from the definition of up-acceptability
 {here also condition 4 is used} that Q n
 is up-bounded. Next, we show that 031{Q n
 }
 up;I is
 smaller than 031{Q
 n0001
 } up;I
 in the lexicographic order. If the relation symbol of L occurs
 inP 011 R then the first component of 031{Q
 n
 } up;I
 becomes smaller because of condition 2.
 Otherwise, if the relation symbol of L occurs in R then the first component
of 031{Q
 n
 }
 up;I
 doesnot increase because of condition 1, while the second one becomes smaller
because of
 condition 3. The conclusion follows from the fact that the lexicographic
ordering is well-
 founded, and from the fact that, in a derivation a constraint can be consecutively
selected
 only a finite number of times. 2
 Example 5.6 {planning is Up-Acceptable} Call R-blocksworld the program ob-
tained from blocksworld by deleting the clauses 6} and 7}. We prove that
planning is
 up-acceptable w.r.t. j j, R-blocksworld,and I defined as in the examples
of Sections 3.1
 192Proving Termination of General Logic Programs
 and 4.1. planning011R-blocksworld is {not incidentally} the program tras.
The proof of up-acceptability proceeds as follows. 1. planning extends R-blocksworld.
 2. It is proven in Section 4.1 that tras is acceptable.
 3. It is proven in Section 3.1 that R-blocksworldacyclic.
 4. Consider a ground instance
 transf orm{c; s; p}   state{s0}; legals{s0; c}; trans{c; s; [s0]; p}:
 of 1}, and suppose that I j= state{s0}. Then
 jtransf orm{c; s; p}j = tot + 3 003 {jcj + 1} + 6 025 3 003 jcj + 2 =
jlegals{s0; c}j. Consider a ground instance
 trans{c; s; v; [ ]}   legals{s; c}:
 of 1}. Then jtrans{c; s; v; [ ]}j = tot 000 card{el{v} \ S } + 3 003
{jcj + 1} + 5 + jvj 025 3003 jcj + 2. 2
 The following corollary establishes the equivalence of the notions of acceptability
and
 up-acceptability. It follows directly from Theorem 5.5 and Theorem 4.6.
 Corollary 5.7 A general logic pro gr am isup-acc eptable if and only if
it is acc eptable.
 6. Weak Up-Acceptability
 Becausein some cases up-acceptability does not help to simplify the proof
of termination,
 in this section we generalize this notion and introduce weak up-acceptability.
We start
 with an example of a program that cannot be split into two non-empty programs
satisfying
 up-acceptability. Next, we introduce weak up-acceptability and establish
analogous results as for up-acceptability. Finally, we apply weak up-acceptability
for simplifying the proof of
 left-termination of our example program.
 6.1 An Example: Hamiltonian Path
 A Hamiltonian path of a graph is an acyclic path containing all the nodes
of the graph. The following program hamiltonian defines hamiltonian paths:
it consists of the following
 clauses
 1} ham{G,P}  path{N1,N2,G,P},
 cov{P,G}. 2} cov{P,G} 
 : notcov{P,G}.
 3} notcov{P,G}  
 193Marchiori
 node{X,G}, : member{X,P}.
 4} node{X,G} 
 member{[X,Y],G}.
 5} node{X,G} 
 member{[Y,X],G}. augmented with the program acypa th defining acyclic paths:
 p1} path{N1,N2,G,P}  path1{N1,[N2],G,P}.
 p2} path1{N1,[N1|P1],G,[N1|P1]}  . p3} path1{N1,[X1|P1],G,P}  
 member{[Y1,X1],G},
 : member{Y1,[X1|P1]},
 path1{N1,[Y1,X1|P1],G,P}.
 p4} member{X,[X|Y]} .
 p5} member{X,[Y|Z]} 
 member{X,Z}.
 A graph is represented by means of a list of edges. For graphs consisting
only of one node, we adopt the convention that they are represented by the
list [[a; ?]], where? is a special new symbol. In the clause p1} path describes
acyclic paths of a graph, and
 path{n1; n2; g; p} calls the query path1{n1; [n2]; g; p}. The second argument
of path1 is used to construct incrementally an acyclic path connecting n1
with n2: using clause p3}, the partial path [xjp1] is transformed into [y;
xjp1] if there is an edge [y; x] in the graph g such that y isnot already
present in [xjp1]. The construction terminates if y isequal to n1,
 because of clause p2}. Thus the relation path1 is defined inductively by
the clauses p2} and
 p3}, using the familiar relation member, specified by the clauses p4} and
p5}. Notice that, it follows from p2} that if n1 and n2 are equal, then [n1]
is assumed to be an acyclic path from n1 to n2, for any g.
 The relation ham{g; p} is specified in terms of path and cov: it is true
if p is an
 acyclicpath of g that covers all its nodes. The relation cov is defined
as the negation of notcov, where notcov{p; g} istrue if there is a node of
g which does not occur in p.
 Finally, the relation node is defined in terms of member in the expected
way. For instance,
 ham{[[a,b],[b,c],[a,a],[c,b]], [a,b,c]} holds, corresponding to the path
drawn in
 boldin the graph of Figure 3.
 The program hamiltonian is not terminating, because acypa th is not. However,
hamiltonian is left-terminating. In order to prove this result using acceptability
{Defini-
 tion 4.2}, we need to find a model of hamiltonian that is also a model of
the completion
 comp{f3}; 4}; 5}; p4}; p5}g} of the program consisting of the clauses 3};
4}; 5}; p4}; p5}. This
 is not very difficult, however it is not needed, as we shall see in the
follow. Note also that
 the notion of up-acceptability does not help to prove left-termination using
less semantic information. Nevertheless, we can split hamiltonian in two
subprograms: P
 2
 consisting of acypa th plus clause 1}, and P
 1
 consisting of the remainingclauses 2} 000 5}. Note that
 P
 2 `almost' extends P
 1 , because P
 1 contains some literals {those with relation fmemberg}
 194Proving Termination of General Logic Programs
bcaFigure 3: The Hamiltonianpath of [[a; b]; [b; c]; [a; a]; [c; b]]
 defined in P
 2
 . Since the subprogram5p}; 6p} definingthese literals is extended by both
P
 1
 and by P
 2
 n f5p}; 6p}g, itfollows that left-terminationof f5p}; 6p}g does not depend
on the terminationbehaviour of the rest of hamiltonian. So, for proving left-termination
of
 hamiltonian it is sufficient to show that P
 2
 011 P 1
 is acceptable, that P
 1
 is acyclic, and that the corresponding level mappings satisfy the condition
in Definition 5.3. Thus, we need
 only to finda modelof P
 2
 011 P 1
 that is also a model of comp{fp4}; p5}g}. 2
 6.2 Weak Up-Acceptability
 Formally , we modify up-acceptability by considering a more general way
of partitioning the
 program, specified using the following notion of weak extension. Recall
that for a set S of
 relations, P
 jS
 denotes the clauses of P that define the relations from S .
 Definition 6.1 {Program Weak Extension} A program P weakly extends a pro
gr am R,
 denoted by P >
 w
 R, if for some set S ofrelations we have that: 
*  P = P
 1
 [P
 jS , and P
 1
 extends P
 jS
 ;
 
*  R extends P
 jS
 ; and 
*  P 011 P
 jS
 extends R 011 P
 jS
 . 2
 Note that only the relations of S which are defined in P play a role in
the above definition.
 Definition 5.1 is a particular case of the above definition, obtained by
considering P
 jS
 to be equal to ; {which includes the case that S = ;}.
 Example 6.2 The program
 p{X}   q{X}, r{X}.
 r{f{X})   r{X}.
 weakly extends the program
 195Marchiori
 q{X}   s{X}, r{X}.
 s{X}  .
 This can be seen by taking S = frg. Then P
 1
 is p{X}   q{X}, r{X}., P
 jS
 is r{f{X})  
 r{X}., P
 1
 and R both extend P
 jS
 . Moreover, P 011 P
 jS is p{X}   q{X}. and R 011 P
 jS
 is
 q{X}   s{X}.
 s{X}  .
 Finally, it is easy to check that P 011 P
 jS extends R 011 P jS
 . 2
 Thus the notion of weak up-acceptability is obtained from Definition 5.3
by replacing in condition 1 `extends' by `weakly extends'.
 Definition 6.3 {Weak Up-Acceptability} Let j j be a level mapping for P
. Let R be a
 set of clauses s.t. P = P
 1
 [ R for some P
 1 , and let I be an interpretation of P 011 R. Pis
 weakly up-acc eptable w.r.t. j j, R and I if the following conditions hold:
1. P
 1
 weakly extends R;
 2. P 011 R is acceptable w.r.t. j j
 jP 011R and I ;
 3. R is acyclic w.r.t. j j
 jR
 ;
 4. for every ground instance H   L 1
 ; : : : ; L n
 of a clause of P
 1
 , for every 1 024 i 024 n,
 
*  if L
 i
 is defined in R and is not a constraint, and 
*  if I j= L
 i1
 ; : : : ; L
 ik
 , where L i1
 ; : : : ; L ik
 are those literals among L
 1
 ; : : : ; L i
 whose
 relations occur in P 011 R, then jH j 025 jL
 i
 j. 2 In order to prove the analog to Theorem 5.5, we need to use triples
of finite multisets,
 instead of pairs, with the lexicographic ordering 036: {X
 1
 ; X
 2
 ; X
 3
 } 036 {Y
 1 ; Y
 2
 ; Y 3
 } iff either {X
 1
 ; X 2
 } 036 {Y 1
 ; Y
 2 } {by abuse of notation we use 036 also to denote the lexicographic ordering
on pairs of multisets}, or X 1
 = Y
 1 and and X
 2
 = Y
 2
 and X
 3
  jL i
 j,
 
*  if L
 i
 is defined in R then jH j 025 jL
 i
 j.
 3. R is acyclic w.r.t. j j. 2
 202Proving Termination of General Logic Programs
 One can check that the results we proved for up-acceptability hold as well
for the above
 definition. In particular, the notion of new up-acceptability is equivalent
to the one of
 acceptability. Note that here we have to find some semantic information
on both the `upper' and the `lower' part of the program; however, information
on the `lower' part is used only
 on the `upper' part of the program. Therefore, also in this case, less semantic
information
 is needed than with the original definition of acceptability by Apt and
Pedreschi. Let us
 illustrate the application of new up-acceptability in the following toy
example.
 Example 8.3 Consider again the program
 1} p   q, p.
 2} q   s.
 We prove that it is new up-acceptable.
 1. The program f1}g extends f2}g;
 2. Consider the level mapping jpj= 1, jqj = 1, jsj = 0, and the interpretations
 I f1}g
 = fpg, I
 f2}g
 = ;.
 Then I
 f1}g
 and I
 f2}g
 are specialized models of f1}g andof f2}g, respectively. We have
 that I
 f1}
 [ I f2}g
 6j= q and jpj= jqj.
 3. From jqj = 1 > 0 = jsj it follows that f2}g is acyclic w.r.t. jj. 2
 Observe that Definition 8.2 is still not applicable in some cases, for instance
to the
 program
 1} p   q, : p.
 2} q   s.
 because the program f1}g 011 f2}g has no specialized model. Another drawback
of our method is its lack of incrementality. Nevertheless, we can
 define an incremental, bottom-up method, where the decomposition step is
applied iter-
 atively to the subprogramsuntil the partition of a subprogram becomes trivial.
This is
 possible because of the equivalence of up-/weak up-/ low-acceptability and
acceptability. These observations are incorporated in the following definition.
Recall that B
 P
 denotes the Herbrand base of P .
 Definition 8.4 {An Incremental Method} 
*  Split P into n 025 1 parts, say P 1
 ; : : : ; P n
 s.t. for every i 2 [1; n 000 1]: { P
 i+1
 {weakly} extends P
 i ;
 { either P i
 or P
 i+1
 is acyclic.
 203Marchiori
 
*  Define incrementally the level mappingj j
 P
 1
 [:::[P
 n
 = j j
 P
 1
 [ : : : [ j j
 P n
 and the inter-
 pretation I
 P
 1 [:::[P
 n = I
 P
 1 [ : : : [ I P
 n
 as follows. 1. {base} If P
 1 is acyclic then find the corresponding level mappingj j
 P
 1 ; otherwise
 provethat P
 1
 is acceptable w.r.t. a level mapping j j
 P
 1 and an interpretation I
 P
 1
 .
 2. {induction} Suppose that j j P
 k
 is defined for every 1024 k 024 i, and suppose that
 I
 P k
 is defined for every 1 024 k < i if P
 i
 is acyclic, and for every 1 024 k 024i if P i
 is
 acceptable, with 1 024 i < n. Then,
 {a} If P
 i+1
 is acyclic then use j j
 P
 i to define a level mapping j j P
 i+1
 for P
 i+1
 011 P
 i
 s.t. P i+1
 011 P i
 is acyclic w.r.t. j j
 P
 i+1 , and s.t. for all ground instances H  
 L
 1
 ; : : : ; L
 m
 of clauses of P
 i+1 , for every 1 024 j 024 m, if L
 j is defined in P
 i then
 jH j
 P
 i+1
 025 jL
 j
 j
 P
 i
 :
 {b} If P
 i
 is acyclic then use j j
 P
 i
 to define a level mapping j j P
 i+1
 for P
 i+1
 011 P
 i
 s.t.:
 i.A. either P
 i+1 011 P
 i
 is acceptable w.r.t. a specialized model I
 P
 i+1
 and
 j j P
 i+1
 ; in this case set I
 P i
 to be B
 P
 i
 ;
 B. or find a specialized model I
 P
 i
 of P
 i
 011 P i0001
 , and a specialized model
 I
 P
 i+1
 of P
 i+1
 011 P
 i
 s.t. for all ground instances H   L
 1 ; : : : ; L
 m of
 clauses of P
 i+1
 and for every 1024 k 024m if L
 k
 is defined in P
 i+1
 then jH j
 P
 i+1
 > jL k
 j
 P
 i+1
 .
 ii. For all ground instances H   L
 1
 ; : : : ; L m
 of clauses of P i+1
 and for every 1 024 k 024m if L
 k
 is defined in P
 i
 then jH j
 P i+1
 025 jL k
 j
 P
 i
 .
 Above,m = min{fmg[ fj 2 [1; m] j I
 P
 1
 [:::[P
 i+1
 6j= L j
 g}:
 2
 We prove that this method is correct, i.e., that P is left-terminating if
the above method is applicable. To deal with non-ground queries, we use the
original notion of boundedness
 by Apt and Pedreschi, this time w.r.t. the interpretation resulting from
the method.
 Definition 8.5 {Bounded Query} Suppose that the partition P
 1
 ; : : : ; P n
 of P , j j
 P
 1
 [:::[P
 n
 and I
 P
 1
 [:::[P
 n
 are obtained using the method of Definition 8.4. Let Q = L
 1
 ; : : : ; L
 m
 . Then
 Q is bounde d {w.r.t. j j and I
 P
 1 [:::[P
 n } if for every 1 024 i 024 m, the set
 jQj
 I
 P 1
 [:::[P n
 i
 = fjL
 0
 i
 j j L
 0
 1
 ; : : : ; L
 0
 n
 is a ground instance of Q and
 I
 P
 1
 [:::[P
 n
 j= L
 0
 1
 ^ : : : ^ L
 0
 i0001
 g
 is finite. 2
 Theorem 8.6 Suppose that the partition P
 1
 ; : : : ; P n
 , j j
 P
 1
 [:::[P
 n
 and I P
 1
 [:::[P
 n
 are obtained
 using the method of Definition 8.4. Let Q be a bounde d query w.r.t. j j
 P
 1
 [:::[P
 n
 and I
 P
 1 [:::[P
 n .
 Then every ldcnf-derivation of Q is finite and it contains only bounde d
queries.
 Pro of. Recall that I
 P 1
 [:::[P n
 = I
 P 1
 [ : : : [ I
 P
 n
 . For a bounded query Q = Q
 1
 ; : : : ; Q m
 , we de-
 fine the n-tuple 031{Q}
 I
 P
 1
 [:::[P
 n
 = {j[Q]j
 I
 P
 n ;P
 n
 011P n0001
 ; : : : ; j[Q]j
 I P
 2
 ;P
 2
 011P
 1 ; j[Q]j
 I
 P
 1
 ;P
 1
 } of multisets, with for a programP , and an interpretation I , j[Q]j
 I ;P = bag{maxjQj
 I
 k
 1 ; : : : ; maxjQj
 I
 k
 m };
 204Proving Termination of General Logic Programs
 whereL
 k
 1
 ; : : : ; L
 k
 m
 are the literals of Q whose relations occur in P . The proof is similar
to
 the one of Theorem 5.5. 2
 In the following section we illustrate the application of this method.
 8.1 An Example: Graph Reduction
 In Example 7.4, a programis described which for a graph g and two nodes
n1 and n2, finds a node n that does not belong to any acyclic path in g from
n1 to n2. Using this program, we define here the program reduce which for
a non-empty graph g andtwo nodes n1 and n2, computes the graph g 0
 obtained from g byremoving all the nodes that do not belong to
 any acyclic path in g from n1 to n2, and all the arcs containing at least
one of such nodes
 {see Figure 5}.
abcabFigure 5: rem{a; b; [[a; b]; [b; c]; [a; a]; [c; b]]; [[a; b]; [a; a]]}
holds The program reduce consists of the clauses:
 1} red{N1,N2,G1,G2}  
 : unif{G1,[]},
 spec{N1,N2,N,G1},
 rem{N,G1,G},
 red{N1,N2,G,G2}. 2} red{N1,N2,G,G}  
 : spec{N1,N2,N,G}.
 3} rem{N,[[X,Y]|G1],G2}  
 member{N,[X,Y]}, rem{N,G1,G2}.
 4} rem{N,[[X,Y]|G1],[[X,Y]|G2]}  
 : member{N,[X,Y]},
 member{N,G1}, rem{N,G1,G2}.
 5} rem{N,[],[]}  .
 6} unif{G,G} .
 205Marchiori
 plus the program specialize. The relation red{n1; n2; g; g
 0
 } is defined by two mutually exclusive cases, corresponding to the clauses
1} and 2}. Clause 1} describes the case where
 there is a node that does not belong to any acyclic path in g from n1 to
n2: first, the
 relation spec is used to find such a node; next, the node and the corresponding
arcs are
 deleted from the graph, using the relation rem; finally, red is called recursively
on the resulting graph. Clause 2} describes the final situation, where g
contains only nodes that
 belongto some of its acyclic paths from n1 to n2 . The relation rem{n; g1;
g2} holds if the graph g2 is obtained from the graph g1 by deleting all the
arcs containing the node n of g1.
 It is recursively defined by the clauses 3}, 4} and 5}, as one would expect.
Observe that queries of the form red{n1; n2; [ ]; g} fail, for every n1;
n2; g. We prove that reduce is left-terminating by using our bottom-up method.
reduce
 can be partitioned in three parts:
 
*  P
 1
 is the program spec1 of Example 7.4;
 
*  P 2
 consists of the clauses 3}, 4}, 5} of reduce plus the clauses 1}, p4}, p5}
of spe-
 cialize;
 
*  P
 3
 consists of the clauses 1}, 2}, and 6} of reduce.
 It is easy to check that P
 2
 is acyclic. Moreover, P
 3
 extends P
 2
 , and P
 2
 weakly extends P
 1
 w.r.t. fmemberg. So we can apply the bottom-up approach to construct a level
mapping j j
 P
 1 [P
 2
 [P
 3
 and an interpretation I
 P
 1
 [P
 2
 [P
 3
 . The proof proceeds as follows.
 
*  P
 1
 is acceptable w.r.t. j j
 P
 1
 and I
 P
 1
 given in Example 7.4.
 
*  P
 2
 011 P 1
 is acyclic w.r.t. jj
 P
 2
 defined as in Example 7.4 for spec and member, and s.t.
 jrem{n; g1; g2}j
 P
 2
 = jg1j + 2. Moreover, clause 1} of specialize satisfies the condition relating
the two level map-
 pings.
 
*  In order to define j j
 P
 3
 , I P
 3
 and I P
 2
 , we apply point i.B. Consider the level mapping jred{n1; n2; g1; g2}j P
 3
 = 3jg1j + 5,
 junif {g; g}j P
 3
 = 0, and let
 I
 P 2
 = frem{n; g1; g2} jg1, g2 lists and either g1= g2 = [ ] or jg2j< jg1jg[
[[spec{X; Y ; Z; W }] [fmember{n;g} j g list and n in set{g}g;
 I
 P
 3 =[red{N 1; N 2; G1; G2}] [ funif {x; y} j x = yg:
 It is easy to check that I
 P
 2
 and I
 P
 3
 are specialized models of P
 2
 011 P
 1 and P
 3
 011 P
 2
 , respectively. It remains to check the tests in points i.B and ii. { Consider
a ground instance red{n1; n2; g1; g2}   :unif {g1; [ ]}; spec{n1; n2; n;
g1};
 rem{n; g1; g}; red{n1; n2; g; g2}:
 206Proving Termination of General Logic Programs
 of 1}. We have that: jred{n1; n2; g1; g2}j P
 3
 = 3jg1j + 5 > 0 = j:unif {g1; [ ]}j
 P
 3 ;
 jred{n1; n2; g1; g2}j
 P
 3
 = 3jg1j + 5 = jspec{n1; n2; n; g1}j
 P
 2
 ;
 jred{n1; n2; g1; g2}j
 P 3
 = 3jg1j + 5 > jg
 1 j + 2 = jrem{n; g1; g}j P
 2
 .
 Now, supposethat I
 P
 2
 [ I
 P
 3
 j= :unif {g1; [ ]}; rem{n; g1; g}. Then g and g1 are lists, g1 6= [ ], and
jgj< jg1j. Then,
 jred{n1; n2; g1; g2}j
 P 3
 = 3jg1j + 5 > 3jgj+ 5 = jred{n1; n2; g; g2}j P
 3
 .
 { Consider a ground instance red{n1; n2; g; g}  :spec{n1; n2; n; g}:
 of 2}. We have that:
 jred{n1; n2; g; g}j
 P
 3
 = 3jgj + 5 = jspec{n1; n2; n; g}j
 P 2
 .
 Observe that the presence of the literal :unif {G1; [ ]} is fundamental
to guarantee left- termination. Without it, left-termination would no longer
hold {take for instance the query
 red{n1; n2; [ ]; g}). 9. Conclusion
 In this paper we proposed simple methods for proving termination of a general
logic pro-
 gram, with respect to SLD-resolution with constructive negation and Prolog
selection rule. These methods combine the notions of acceptability and acyclicity.
They provide a more
 practical proof technique for termination, where the semantic information
used is minimal-
 ized. We have illustrated the relevance of the methods by means of some
examples, showing
 in particular that SLD-resolution augmented with Chan's constructive negation
is powerful
 enough to formalize and implement interesting problems in non-monotonic
reasoning. We would like to conclude with an observation on related work.
Apt and Pedreschi
 {1994} introduceda modular approach for proving acceptability of logic programs,
i.e., they
 do not deal with programs containing negated atoms. Proving termination
of general logic
 programs in a modular way, usingthe notion of acceptability, seems a rather
difficult task, because it amounts to buildinga model of the completion of
a program by combiningmodels
 of the completionsof its subprograms. Apt and Pedreschi do not tackle this
problem. In
 this paper, we have provided an alternative way of proving termination w.r.t.
the Prolog selection rule, where one tries to simplify the proof by using
as little semantic information
 as possible, possibly in an incremental way using the methodology illustrated
in Section 8.
 Acknowledgements
 This research was partially supported by the Esprit Basic Research Action
6810 {Compulog
 2}. I would like to thank Jan Rutten for proof reading this paper, Krzysztof
Apt for propos-
 ing the study of acyclic and acceptable programs, Frank Teusink for pleasant
discussions, as well as the anonymous referees for useful suggestions and
comments on an earlier version
 of this paper.
 207Marchiori
 References Apt, K., & Bezem, M. {1991}. Acyclic programs. New Generation
Computing, 9, 335{363.
 Apt, K., & Bol, R. {1994}. Logic programming and negation: a survey. The
Journal of
 Lo gic Pro gr amming, 19-20, 9{71. Apt, K.,& Pedreschi, D. {1991}. Proving
termination of general prolog programs. In
 Pro c e e dings of the Int. Conf. on Theor etic al Aspe cts of Computer
Software, Vol. LNCS
 526, pp. 265{289. SpringerVerlag.
 Baral, C., & Gelfond, M. {1994}. Logic programming and knowledge representation.
The
 Journal of Lo gic Pro gr amming, 19-20, 73{148. Bratko, I. {1986}. PROLOG
Pro gr amming for Artificial Intel ligence. Addison-Wesley . Chan, D. {1988}.
Constructive negation based on the completed database. In Pro c e e dings
 of the 5th Int. Conf. and Symp. on Lo gic Pro gr amming, pp. 111{125. Clark,
K. {1978}. Lo gic and Databases, chap. Negation as Failure, pp. 293{322.
Plenum
 Press, NY.
 De Schreye, D., & Decorte, S.{1994}. Termination of logic programs: The
never-ending story. The Journal of Lo gic Pro gr amming, 19-20, 199{260.
 Dershowitz, N.{1987}. Termination of rewriting. Journal of Symbolic Computation,
3,
 69{116.
 Evans, C. {1990}. Negation as failure as an approach to the hanks and mcdermott
problem.
 In Pro c e e dings of the 2nd International Symposium om AI, pp. 23{27.
Kowalski, R., & Sergot, M. {1986}. A logic based calculus of events. New
Generation
 Computing, 4, 67{95.
 Marchiori, E. {1995}. A methodology for proving termination of general logic
programs.
 In Pro c e e dings of the 14th International Joint Conferenc e on Artificial
Intel ligence
 {IJCAI'95}, pp. 356{367.
 Marchiori, E. {1996}. On termination of general logic programs w.r.t. constructive
negation.
 The Journal of Lo gic Pro gr amming, 26{1}, 69{89.
 McCarthy, J.,& Hayes, P. {1969}. Some philosophical problems from the standpoint
of
 artificial intelligence. Machine Intel ligence, 4, 463{502.
 Nilsson, N. {1982}. Principles of Artificial Intel ligence. Springer-Verlag.
Sterling, L., & Shapiro, E. {1994}. The Art of Prolo g. MIT Press.
 208