E. Marchiori

Volume 4, 1996

**Links to Full Text:**

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.

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 3jL 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