A Methodology for Proving Termination of General Logic Programs

1 Introduction

General logic programs (glp's for short) provide formal­ izations and implementations for special forms of non­ monotonic reasoning. For example, the Prolog negation as finite failure operator has been used to implement a formulation as logic program of the temporal persistence problem in AI (see l9; 8; 1]). Termination of glp's is a relevant topic (see [7]), also because the implementation of the operators for the negation, like Clark's negation as failure [5] and Chan's constructive negation [4], are based on termination conditions. Two typical examples of glp's which behave well w.r.t . termination are the so­ called acyclic and acceptable programs ([1], [2]). In fact, it was proven in [1] that when negation as finite failure is incorporated into the proof theory, a program is acyclic iff all sld-derivations with arbitrary selection rule of non­ floundering ground queries are finite. Floundering is an abnormal form of termination which arises as soon as a non-ground negative literal is selected. A similar result was proven in [2] for acceptable programs, this time with the selection rule restricted to be the Prolog one, which selects always the leftmost literal of a query. In [10] it was shown how one can obtain a complete characteri­ zation (i.e. to overcome the drawback of floundering) by considering Chan's constructive negation procedure instead of negation as finite failure.

The notion of acceptability combines the definition of acyclicity with a semantic condition, that uses a model of the program which has also to be a model of the comple­ tion of its "negative part" (see Definition 3.2). Because of this semantic condition, the proof of acceptability may become rather cumbersome. Moreover, finding a model which satisfies the above requirement may be rather dif­ ficult.

In this paper we refine the notion of acceptability, by using a semantic condition which refers only to that part of the program which is not acyclic. More specifically, a program P is split into two parts, say P1 and P2; 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 Pro­ leg selection rule. The decomposition of P is done in such a way that no relations defined in P1 occur in P2 . We introduce the notion of up-acceptability, where P1 is proven to be acceptable and P2 to be acyclic, and the one of low-acceptability which treats the converse case (P1 acyclic and P2 acceptable). We illustrate the useful­ ness of this approach by means of examples of programs which formalize problems in non-monotonic reasoning.

Even though our main results deal with Chan's con­ structive 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 prov­ ing termination of glp's, which combines the results of Bezem, Apt and Pedreschi on acyclic and acceptable pro­ grams, results widely considered as a main theoretical foundation for the study of termination of logic programs ([7]). We believe that this methodology is relevant for at least two reasons: it overcomes the drawback of [2] for proving termination due to the use of too much semantic information, and it allows to identify for which part of the program termination does or does not depend on the fixed Prolog selection rule.

The remaining of this paper is organized as follows. The next section contains some preliminaries; in Section 3 we explain the notions of acyclicity and acceptability. In Section 4, the notions of up- /low-acceptability are introduced. In Section 5, we introduce a methodology for proving termination of glp's, based on these notions. Finally, in Section 6 we give some examples. For lack of space, proofs of the results have been omitted. They can be found in the full version of the paper.

2 Preliminaries

We follow Prolog syntax and assume that a string start­ ing with a capital letter denotes a variable, while other strings denote constants, terms and relations. A {ex­ tended} general logic program, called for brevity pro­ gram and denoted by P, is a finite set of (universally quantified) clauses of the form H +- L1, ... , Lm, where m ;:: 0, H is an atom, and the Li's, called literals, are either atoms p(s) , or negative literals ·p(s), or equali­ ties s = t, or inequalities 'V(s =/: t), where 'V quantifies over some (perhaps none) of the variables occurring in the inequality. Equalities and inequalities are also called constraints, denoted by c. An inequality 'V( s =f:. t) is said to be primitive if it is satisfiable but not valid. For in­ stance, X =f:. a is primitive. In the following, the letters A, B indicate atoms, while C and Q denote a clause and a query, respectively.

Suppose that all sld-derivations of Q are finite and do not involve the selection of any negative literals. Then there is a finite number of computed answer substitu­ tions, say lh, ... ,(h, k 2: 0; let FQ be the equality formula 3(Ee 1 V ... V Eek ), where Ee 1 is the substi­ tution fh written in equational form, and 3 quantifies over the variables that do not occur in Q. Then the Clark's completion of P logically implies 'V( Q +-+ FQ ), i.e., comp(P) I= 'V(Q +-+ FQ)· To resolve negative non­ ground literals, Chan in [4] introduced a procedure, here called sldcnf-resolution, where the answers for ·Q are obtained from the negation of F Q. However, this pro­ cedure is undefined when Q has an infinite derivation. Then, the notion of (infinite) derivation in this setting is not always defined. Therefore in this paper we refer to an alternative definition of the Chan's procedure intro­ duced in [10], where the subsidiary trees used to resolve negative literals are built in a top-down way, construct­ ing their branches in parallel. We shall also consider a fixed selection rule, where at every resolution step, the leftmost possible literal is selected, where a literal is called possible if it is not a primitive inequality. Intu­ itively, the selection of primitive inequalities is delayed until their free variables become enough instantiated to render the inequalities valid or unsatisfiable. We call with slight abuse Prolog selection rule this selection rule. Then sldcnf-trees with Prolog selection rule are called ldcnf-trees.

To prove termination of logic programs, functions called level mappings have been used [1], which map ground atoms to natural numbers. Their extension to negated atoms was given in [2], where the level mapping of ..,A is simply defined to be equal to the level mapping of A. Here, we have to consider also constraints. Con­ straints are not themselves a problem for termination, because they are atomic actions whose execution always terminates. Therefore, we shall assume that the notion of level mapping is only defined for literals which are not constraints. However, note that the presence of con­ straints in a query influences termination, because for instance a derivation fails finitely if a constraint which is not satisfiable is selected.

Definition 2.1 (Level Mapping) A level mapping is a function I I from ground literals which are not constraints to natural numbers s.t. I·AI = IAI .

In the following sections we introduce the notions of acyclic and acceptable program.

3 Acyclic and Acceptable Programs

In this section, the definitions of acyclic and acceptable program are given, together with some useful results from [10] .

Definition 3.1 (Acyclic Program) A program P is acyclic w. r. t. a level mapping I I if for all ground in­ stances H +- £1 , ... , Lm of clauses of P we have that IHI > ILil holds for every i E [1, m] s.t . Li is not a con­ straint. P is called acyclic if there exists a level mapping II s.t . Pis acyclic w.r.t. II·

With a query Q = £1, .. . , Ln we associate n sets IQi i of natural numbers s.t .

Q is called bounded w.r.t. II if every IQii is finite.

Bounded queries characterize a class of queries s.t. ev­ ery their sldcnf-derivation is finite. We have proven in [10] that if P is acyclic and Q is bounded then every sldcnf-tree for Q in P is finite; and that also the con­ verse of this result holds: call a program P terminating if all sldcnf-derivations of ground queries are finite . Then, for a terminating program P, there exists a level map­ ping II s.t.: (i) Pis acyclic w.r .t . I I; (ii) for every query Q, Q is bounded w.r.t. I I iff all its sldcnf-derivations are finite. Notice that when negation as finite failure is assumed, (i) holds only if Q does not flounder ([1]). In fact, simple programs, like

terminate because floundering, but are not acyclic.

For studying termination of general logic programs with respect to the Prolog selection rule, the notion of acceptable program ([2]} was introduced. Its defi­ nition is based on the same condition used to define acyclic programs, except that, for a ground instance H +- £1, .. . , Ln of a clause, the test IHI > ILil is per­ formed only till the first literal Ln: which fails. This is sufficient since, due to the Prolog selection rule, literals after Ln: will not be executed. To compute n, a class of models of P, here called good models, is used. A model of P is good if its restriction to the relations from N egj, is a model of comp(P-}, where p- is the set of clauses in P whose head contains a relation from N egj,, and N egj, is defined as follows. Let N egp denote the set of relations in P which occur in a negative literal in the body of a clause from P. Say that p refers to q if there is a clause in P that uses the relation p in its head and q in its body, and say that p depends on q if (p, q) is in the reflexive, transitive closure of the relation refers to. Then N egj, denotes the set of relations in P on which the relations in N egp depend on.

Definition 3.2 (Acceptable Program) Let I I be a level mapping for P and let I be a good model of P. P is acceptable w.r .t . I I and I if for all ground instances H +- £1, ... , Ln of clauses of P we have that

holds for i E [1, n] s. t. Li is not a constraint, where n = min({n} U {i E [1,n]l I~ Li}).

P is called acceptable if it is acceptable w. r. t. some level mapping and a good model of P .

Let Q = L1, ... , Ln be a query, let I I be a level map­ ping and let I be a good model of P. Then, with Q we associate n sets of natural numbers s.t . fori E [1, n],

Then Q is called bounded if every IQI[ is finite.

Bounded queries characterize those queries s.t. all their ldcnf-derivations are finite. In [10], we have shown that similar results as those for terminating pro­ grams hold also for left-terminating programs, where a program is left-terminating if all ldcnf-derivations of ground queries are finite.

4 Up- and Low-Acceptability

To prove that a program P is acceptable is in general more difficult than to prove that it is acyclic, because one has to find a good model of the program. Therefore in this section we introduce two equivalent definitions of acceptability, called up- and low-acceptability, which are simpler to be used, since one has only to find a good model of a subprogram, which is obtained discarding those clauses forming an acyclic program. Informally, to prove that a program is left-terminating, it is decom­ posed into two suitable parts: then, one part is shown to be acyclic and the other one acceptable. The following notion is used to specify the relationship between these two parts. Recall that a relation is said to be defined in a program if it occurs in the head of at least one clause of the program.

Definition 4.1 Let P and R be two programs. We say that P extends R, written P > R, if no relation defined in P occurs in R.

Informally, P extends R if P defines new relations pos­ sibly using the relations defined already in R. Then one can imagine the program P U R as formed by an upper part P and a lower part R, and investigate the cases when either the lower or the upper part of the program is acyclic. This is done in the following sections, by in­ troducing the notions of up- and low-acceptability. For a level mapping I I, we shall denote by IIIR its restriction to the relations defined in the program R.

In the following definition, the upper part of the pro­ gram is proven to be acceptable and the lower part to be acyclic. For two programs P, R, let P \ R denote the program obtained from P by deleting all clauses of R and all literals defined in R.

Definition 4.2 (up-acceptability) Let I I be a level mapping for P. Let R be a set of clauses s.t. P = P1 UR for some P1, and let I be an interpretation of P \ R. P is up-acceptable w.r.t. I I, R and I if the following conditions hold:

1) P1 extends R; 2) P\R is acceptable w.r .t . IIIP\R and I ; 3) R is acyclic w.r.t . IIIRi 4) for every ground instance H- L1, . .. , Ln of a clause of P1, fori E [1, n] , if L; is defined in Rand is not a constraint, then IHI ~ IL; I.

A program is called up-acceptable if there exists II, R and I s.t . Pis up-acceptable w.r .t . II, Rand I .

Observe that for R equal to the empty set of clauses, we obtain the original definition of acceptability. Now, we introduce the notion of up-bounded query. Suppose that Pis up-acceptable w.r.t. II, Rand I . Consider a query Q = L1, .. . , Ln. Then, with Q we associate n sets of natural numbers s.t . fori E [1, n],

where L~ 1 , ·· · , L~ 1 are all those literals of L~, . .. , L~-l (whose relations are) defined in P1. Then Q is called up­ bounded if every IQI7p,I is finite. The following result holds.

Theorem 4.3 Suppose that P is up-acceptable w.r.t. II , R and I. Let Q be an up-bounded query. Then every ldcnf-tree for Q in P contains only up-bounded queries and is finite.

The following corollary establishes the equivalence of the notions of acceptability and up-acceptability.

Corollary 4.4 Let P be a general logic program. Then: (i) If P is up-acceptable then P is acceptable. (ii) If P is acceptable then it is up-acceptable.

Now, we consider the converse case, where the lower part of the program is proven to be acceptable and the upper part to be acyclic.

Definition 4.5 (low-acceptability) Let I I be a level mapping for P. Let R be a set of clauses s.t . P = P1 U R for some P1, and let I be an interpretation of R. P is low-acceptable w. r. t. I I, R and I if the following conditions hold: 1) P1 extends R; 2) P \ R is acyclic w.r.t . I IIP\Ri 3) R is acceptable w.r .t . I IIR and I; 4) for every ground instance H - L1, ... , Ln of a clause of P1, for i E [1, n], if L; is defined in R and is not a constraint, then IHI ~ IL; I.

A program is low-acceptable if there exists I I, R and I s.t. Pis low-acceptable w.r .t .ll, Rand I .

Suppose that P is low-acceptable w.r.t. I I, R and I. Then the notion of low-boundedness is defined as in the previous section, where IQI7p,I is replaced by the set

where L~ 1 , ··· , L~, are all those literals of L~ , . .. , L~- l (whose relations are) defined in R. Then the correspond­ ing of Theorem 4.3 and Corollary 4.4 hold, where up is replaced by low .

5 A Methodology

Definitions 4.2 and 4.5 provide us with a method for proving left-termination of general logic programs. For a program P, the method can be informally illustrated as follows:

1. Find a maximal set R of clauses of P s.t . R forms an acyclic program and P = P1 URis s.t. either P1 extends R or vice versa.
2. If R extends P1 then:

• 2.1) Prove that P \ R is acceptable w.r.t . a level map­ ping, say 111, and an interpretation.
• 2.2) Use ll1 to define a level mapping ll2 for R s.t. R is acyclic w.r.t. I l2 , and s.t. for every ground instance H +- L1, ... , Ln of a clause of R, if L; is defined in P1 and it is not a constraint, then IHI2 ~ IL;Il holds.
• If P1 extends R then:
• 3.1) Prove that R is acyclic w.r .t. a level mapping, say I h·

3.2) Use I l1 to define a level mapping I l2 for P \ R s.t. P \ R is acceptable w.r .t. I l2 and an interpreta­ tion, and s.t . for every ground instance H +- L1. .. . , Ln of a clause of P1 , if L; is defined in R and it is not a constraint, then IHI2 ~ IL;I1 holds.

This method overcomes a drawback of the original method of Apt and Pedreschi to prove left-termination, where one has to find a good model of all the program.

A drawback of our method one immediately observes is its lack of incrementality. In fact, it would be nice to have an incremental, bottom-up method, where the decomposition step 1. is applied iteratively to the sub­ programs until possible (i.e., until the partition of a sub­ program becomes trivial) . This is possible, because a program is up- /low-acceptable iff it is acceptable. Then in the conditions 2 of Definition 4.2 and 3 of Definition 4.5 we can prove up-/low-acceptability instead of accept­ ability. The resulting method is informally illustrated as follows.

• Find a partition of P, say P1. ... , Pn s.t. for every i E [1, n- 1]: - Pi+l > P; (Pi+1 extends P;); - either P; or Pi+l is acyclic; and - if Pi+l is acyclic then it is a maximal set of clauses from P1 U ... U Pi+l which forms an acyclic program.
• Prove that for every i E [1, n], the program Po U ... UP; is up- or low-acceptable.

We can prove that Po U ... U P; is up- or low-acceptable in an incremental way, as follows. Suppose that for an i < n, P1 U .. . UP; has been proven up- or low-acceptable w.r.t . l l1 and I. Then:

2) If P; is acyclic then use ll1 to define a level mapping l l2 for Pi+l \ P; s.t . Pi+l \ P; is acceptable w.r.t . ll2 and an interpretation, and s.t. for every ground instance H +- L1 , . .. , Ln of a clause of Pi+b if Lj is defined in P; and it is not a constraint , then IHI2 ~ ILill holds.

1) If P;+l is acyclic then use I I i to define a level mapping l l2 for P;+l \P; s.t. P;+l \P; is acyclic w.r.t. 112, and s.t. for every ground instance H +- L1, . . . , Ln of a clause of P;+l , if Lj is defined in P; and it is not a constraint, then IHI2 ~ ILi l1 holds.

Observe that by using this incremental bottom-up ap­ proach, one obtains the subprogram R to be used to prove up- /low-acceptability (either P1 or Pn), together with a potential level mapping I I (the union of the level mappings of the P;'s). However, the interpretation I is not obtained. Thus this method is less powerful than the non-incremental one, because it does not allow to deal with non-ground queries (by means of the notion of boundedness) except for those consisting of only one literal. ·

Apt and Pedreschi in [3] introduced a modular ap­ proach for proving acceptability of pure Prolog programs, i.e. without negation. The extension of this approach to programs containing negated atoms is not treated, and also our method does not solve this problem. Instead, our approach provides an alternative methodol­ ogy for proving acceptability, where one tries to simplify the proof by using as minimal semantic information as possible.

6 Application

In this section we illustrate by means of some examples how various problems in non-monotonic reasoning can be formalized by means of acyclic or acceptable programs. We consider the blocks-world problem, planning in the blocks-world, and search in graph structures.

Blocks World

The blocks world is a formulation of a simple problem in AI, where a robot is allowed to perform a number of primitive actions in a simple world (see e.g. [11]) . Here we consider a simple version of this problem, where there are three blocks, say a, b, c, and three different places of a table, say p, q and r. A block is allowed to lay either above another block or on one of these places. Blocks can be moved from one to another location. The problem consists of specifying when a configuration in the blocks world is possible, i.e., if it can be obtained from the initial situation by performing a sequence of possible moves. We use McCarthy and Hayes situation calculus to formulate the problem, in terms of facts , events and situations. One can distinguish three types of facts: loc(X, L) stands for a block X is in the location L; on( X , Y) for a block X is on a block Y ; and clear( L) for there is no block in the location L . It is sufficient to con­ sider only one type of event, namely move a block X into a location L, denoted by move( X , L) . Finally, we repre­ sent situations by means of lists: [] stands for the initial situation, and [XeiXs] for the one corresponding to the occurrence of the event X e in the situation X s. Based on the above representation, one can formalize the blocks world by means of the following program blocks-world, where top(X) denotes the top of the block X, and B = {a,b, c}, P = {p,q , r,top(a),top(b),top(c)}, and .C = {loc(a,p) , loc(b, q),loc(c,r)}:

• (loc) holds(l,[]) +-. lE.C
• (blo) block(bl) +- . bl E B
• (pla) place(pl) +- . pl E P
• (hl) holds(loc(X,L),[move(X,L)IXs]) +­ block(X), place(L), holds(clear(top(X)),Xs), holds(clear(L),Xs), L =/= top(X). (h2) holds(loc(X,L),[XeiXs]) +­ block(X), place(L), ~ abnormal(loc(X,L),Xe,Xs), holds(loc(X,L),Xs).
• (h3) holds(on(X,Y),Xs) +­ holds(loc(X,top(Y)),Xs).
• (h4) holds(on(X,Y),Xs) +­ holds(loc(X,top(Z)),Xs), holds(loc(Z,top(Y)) ,Xs).

(h5) holds(clear(L),Xs) ~ -. busy(L,Xs). (ab) abnormal(loc(X,L), move(X,L'),Xs) ~. (bu) busy(L,Xs)~ holds(loc(X,L),Xs). (st) legal-s( [(a,L1), (b,L2), (c,L3)] ,Xs) ~ holds(loc(a,Ll),Xs), holds(loc(b,L2),Xs), holds(loc(c,L3),Xs).

The initial situation is described by clauses (loc). The relation holds is used to describe when a fact is pos­ sible in a certain situation, while the relation legal-s specifies when a configuration is possible in a certain sit­ uation. It is easy to check that blocks-world is acyclic w.r.t. the following level mapping [[, where we use the function II from ground terms to natural numbers s.t. if y is a list then Jyj is its length, otherwise Jyj is 0.

{ 3 * JyJ + 1 3 * JyJ + 3 Jholds(x, y)J = ~ * JyJ + 4 Jbusy(x, y)J = 3 * JyJ + 2, Jblock(x)J = 0, Jplace(x)J = 0, Jabnormal(x, y, z)J = 0, [legal- s(x, y)J = 3 * JyJ + 2. if x of form loc(r, s) , if x of form clear(r, s), if x of form on(r, s) , otherwise.

Consider for instance the query holds (on(a, Y), [Xs]): it is bounded, hence every its sldcnf-derivation is finite. We obtain the answers (Y = b 1\ X s =move( a, top(b))) and (Y = c 1\ X s =move( a, top( c))).

Planning in the Blocks World

We consider now plan-formations in the blocks world, which amounts to the specification of a sequence of pos­ sible moves which yield a particular configuration. This problem can be solved by means of a nondeterministic algorithm ([12)): while the desired state is not reached, find a legal action, update the current state, check that it has not been visited before. The following program planning follows this approach, where the clauses of blocks-world which define the relation legal-s, whose union is denoted by r-blocks-world, are supposed to be included in the program, Note that here the initial con­ figuration is any situation which can be reached from the initialization (which is described by the clauses (loc) of blocks-world) . Alternatively, as done in [12], one could let unspecified the initialization, which would be provided every time the program is tested.

• (t) transform(Xs,St,Plan) ~ state(StO), legal-s(StO,Xs),
• trans(Xs,St,[StO],Plan). (tl) trans(Xs,St,Vis, [ ]) ~ legal-s(St,Xs). (t2) trans(Xs,St,Vis,[ActiActs]) ~ state (St1) , -. member(Stl,Vis), legal-s(Stl,[ActiXs]), trans([Act1Xs],St,[St11Vis],Acts). (s) state( [(a,L1), (b,L2), (c,L3)]) ~ Pz[p,q,r,top(a),top(b),top(c)], member(Ll,P), member(L2,P), member(L3,P).

(ml) member(X, [XIY]) ~. (m2) member(X,[YIZ]) ~ member(X,Z).

To prove that planning is left-terminating using Defini­ tion 3.2 is rather difficult, because it requires to find a model of planning, which is a model of the completion of the program consisting of the clauses (m1) and (m2) and of all the clauses of blocks-world, but (h3), (h4), ( st).

We prove that planning is up-acceptable w.r.t. I [, r-blocks-world, and I defined as follows. The level mapping I I for planning is the one of the previous exam­ ple when restricted to r-blocks-world, and is defined as follows for the other relations.

Jtransform(x, y, z)j = N + 3 * (Jxj + 1) + 2 + 3 + 1; Jtrans(x, y, z, w)J = N- card(el(z) n S) + 3 * (Jxj + 1) + 2 + 3 + jzj ; Jstate(x)[ = 7; Jmember(x, y)J = JyJ .

Here el(z) denotes set(z) if z is a list, the empty set otherwise; card(el(z) n S) is the cardinality of the set el(z) n S; JxJ is defined as in the previous ex­ ample; and N denotes the cardinality of S . Note that (N- card(el(z) n S) is greater or equal than 0. Then I I is well defined. Let tras be the program planning\r-blocks-world. We consider the following interpretation I of tras: let set(y) be the set of ele­ ments of the list y, and S = {[(a,p1), (b, p2), (c,p3)] I fori E [1, 3],pi E {p, q, r, top( a), top(b), top( c)}}.

!transform = [transform( X, Y, Z)] , Itrans = [trans( X, Y, Z, W)], I member= {member(x, y) I y list s.t. x E set(y)}, lstate = {state(x) [ XES}.

Then I= !transform U Itrans U I member U I state· It is easy to prove that I is a model of tras. Moreover, N egP\R = {member} , and tras- is equal to {(m1) , (m2)}. Then it is easy to check that I restricted to {member} is a model of comp(tras-) . Moreover, conditions 1-4 of up­ acceptability are satisfied: for instance, the proof of con­ dition 2 (tras is acceptable w.r.t. I and [I) is based on the following properties of[[: Jtransform(x, y, z)j 2: 8, Jtrans(x, y, z , w)J2: 8, and Jtrans(x, y , z , w)J > jzl) . Consider the query transform( [ ] , st ,Plan), where st is a given state. This query is up-bounded, hence by The­ orem 4.3 all its ldcnf-derivations are finite, and produce a plan of actions which transforms the initial state [ ) into the final one st. Notice that this query has an infinite sldcnf-derivation, whiCh is obtained by selecting always the rightmost literal of the clause ( s ).

Search in Graph Structures

Graph structures are used in many applications, such as representing relations, situations or problems. Two typical operations performed on graphs are find a path between two given nodes , and find a subgraph with some specified properties. The following program specialize is an example of the combination of these two operations.

The relation spec is specified by clause (a), as the negation of another relation, called unspec, where unspec( n1, n2, n, g) is true if there is an acyclic path of the graph g connecting the nodes n1 and n2 and containing n. Acyclic paths of a graph are described by the relation path, defined by the clause (c), where path(n1,n2,g,p) calls the query path1(n1, [n2],g,p). Here the second argument of path1 is used to construct incrementally a path connecting n1 with n2: using clause (e), the partial path [xlp1] is transformed in [y, xlp1] if there is an edge [y, x] in the graph g such that y is not already present in [xlp1]. The construction terminates if y is equal to n1, thanks to clause (d) . The relation path1 is defined inductively by the clauses (d) and (e), using the familiar relation member, specified by the clauses (f) and (g) .

Notice that, from (d) it follows that if n1 and n2 are equal, then [n1] is assumed to be an acyclic path from nl to n2, for any g.

• (a) spec(Nl,N2,N,G) ~ .., unspec(Nl,N2,N,G).
• (b) unspec(Nl,N2,N,G) ~ path(Nl,N2,G,P),
• member(N,P). (c) path(Nl,N2,G,P) ~ pathl(Nl,[N2],G,P). (d) pathl(Nl,[NliPl],G,[NliPl]) ~. (e) pathl(Nl, [XliPl] ,G,P) ~ member([Yl,Xl],G), .., member(Yl,[XliPl]), pathl(Nl,[Yl,XliPl] ,G,P) . (f) member(X,[XIYJ) ~ . (g) member(X, [Y I Z]) ~ member(X,Z).

Here a graph is represented by means of a list of edges. For instance spec(a, b,c, [[a, b], [b,c], [a,a]]) holds, where a, b, c are constants and the graph [[a, b], [b, c], [a, a]] is repre­

sented below.

Observe that specialize is not terminating: for in­ stance, the query pathl (a, [b, c] , d, e) has an infinite derivation obtained by choosing as input clause (a vari­ ant of) the clause (e) and by selecting always its right­ most literal.

However specialize is left-terminating. Note that to prove this result using Definition 3.2 requires to find a suitable model of the completion of the program, which is rather difficult . Therefore we prove left-termination by means of low-acceptability.

We prove that specialize is low-acceptable w.r.t. II, specl and I, defined as follows. specl is the program consisting of the all the clauses of specialize but (a) . Let spec2 be the program consisting of the clause (a) of specialize. Define the level mapping II as follows:

lspec(n1, n2, n, g)l = lunspec(n1, n2, n, g)l + 1, lunspec(n1, n2, n, g)l = 0, lmember(s, t)l = ltl; lpath1(n1,p1, g,p)l = IP11 + lgl + 2(lgi-IP1 n gl) + 1, lpath(n1,n2,g,p)l = 3lgl +3, lunspec(n1, n2, n, g)l = 3lgl + 4,

where for two lists p and g p n g denotes the list con­ taining as elements those x which are elements of p and such that there exists a y s.t . [x, y] is an element of g.

Let I= Iunspec U lpath U lpathl U !member, where:

lunspec = [unspec(N1, N2, N, G)], lpath = {path(n1,n2,g,p) I lgl + 1 ~ IPI}, lpathl = {path1(n1,p1,g,p) I IP11-IP1 n gl ~ IPI-IP n gl}, !member= {member(s, t) I t list s.t. s E set(t)}.

It is easy to prove that I is a model of specl . Moreover N eg;pecl = {member} and specl- = { (!), (g)} . Then I restricted to member is a model of comp( specl-).

Conditions 1-4 of the definition of low-acceptability are easy to check. Consider now the query Q = spec(a,b,X, [[a, b), [b,c], [a,a]]). It is low­ bounded. Then one obtains a finite ldcnf-tree for Q, with answer (X =/= a 1\ X =/= b) . Notice that by using negation as failure Q does flounder.

Acknowledgments

I would like to thank Krzysztof Apt, Jan Rutten, and Frank Teusink, and the referees. This research was partly supported by the Esprit Basic Research Action 6810 (Compulog 2).