\documentstyle[jair,twoside,11pt,theapa]{article}
\input epsf 


\jairheading{4}{1996}{179-208}{11/95}{4/96}
\ShortHeadings{Proving Termination of  General Logic Programs}{Marchiori}
\firstpageno{179}

\newcommand{\Proof}{\NI
                    {\it Proof.}\ }
\newtheorem{theorem}{{Theorem}}[section]
\newtheorem{defined}[theorem]{{Definition}}
\newenvironment{definition}{\begin{defined} \rm}{\end{defined}}
\newtheorem{exa}[theorem]{{Example}}
\newenvironment{example}{\begin{exa} \rm}{\end{exa}}
\newtheorem{proposition}[theorem]{{Proposition}}
\newtheorem{conjecture}[theorem]{{Conjecture}}
\newtheorem{lemma}[theorem]{{Lemma}}
\newtheorem{corollary}[theorem]{{Corollary}}
\newtheorem{remark}[theorem]{{Remark}}
\newtheorem{fact}{{Fact}}
\newtheorem{claim}{{Claim}}
\newtheorem{exe}{{Exercise}}
\newenvironment{exercise}{\begin{exe} \rm }{\end{exe}}

 \newenvironment{program}{\tt \begin{tabbing}pro\= {\tt pro}\= {\tt pro}\=clause \kill}{\end{tabbing}}

\newcommand{\Graphb}[3]%
{\begin{figure}[htpb]%
\vspace{5mm}%
        \epsfxsize#2%
        \centerline{\ \epsfbox{#1}\ }%
\vspace{1mm}
\begin{center}
\mbox{{#3}}%
\end{center}
\vspace{5mm}%
 \end{figure}%
} 
\long\def\comment#1{}
\newcommand{\setminusp}{\ominus}
\newcommand{\IFF}{\leftrightarrow}
\newcommand{\la}{\leftarrow}
\newcommand{\NI}{\noindent}
\newcommand{\true}{{\it true}}
\newcommand{\false}{{\it false}}
 \newcommand{\HB}{\hfill{$\Box$}}
\newcommand{\VV}{\vspace{5 mm}}
\newcommand{\good}{ specialized  }
\begin{document}


\title{Practical Methods for Proving Termination of\\ General Logic Programs}

\author{\name Elena Marchiori \email elena@cwi.nl \\
       \addr Centrum voor Wiskunde en Informatica (CWI) \\
       P.O. Box 94079, 1090 GB Amsterdam, 
     The Netherlands}

% For research notes, remove the comment character in the line below.
% \researchnote

\maketitle

\begin{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.
\end{abstract}


\section{Introduction}\label{sec:intro} 
   General logic programs ({\sc {\sc glp\/}\/}'s for short)
 provide formalizations and implementations for special forms
 of non-monotonic reasoning, 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
    \cite{ks86,ev90,ab}.  
  The implementation
    of   operators  like Clark's  
    negation as failure \cite{cl78} and  
     Chan's constructive negation \cite{chan}, is based on  
  termination conditions. 
  Therefore the study of termination of {\sc glp\/}'s (e.g.,
  De Schreye \& Decorte, 1994) is an important topic.

  Two classes of   {\sc glp\/}'s that behave well
 w.r.t.\ termination are the so-called
 acyclic  and acceptable programs \cite{ab,ap91}. 
  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) establish    analogous 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 termination which arises as soon
 as a non-ground negated atom is selected, as explained e.g., in 
 \cite{ab94}.
 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. 
   

  
 The notion of  acceptability   combines 
 the definition of acyclicity with a semantic condition, 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 defined in $P_1$ occur in $P_2$.
 We introduce the notions of
 {\em up-acceptability}, where $P_1$ is proven to be acceptable
 and $P_2$ to be acyclic, and   of  
 {\em low-acceptability}, 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  {\em weak  up-acceptability\/}.
 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 {\em 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 \ref{mod},  \ref{w-mod} and \ref{modlo}) deal  with
   Chan's constructive 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 {\sc glp\/}'s, by combining 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 dependent on the use of the
   Prolog selection rule.  
  Moreover, the examples
   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 \ref{subsec:acy} and  \ref{subsec:acc}
 the notions of acyclicity and acceptability are presented.
   Sections \ref{sec:up},  \ref{sec:weakly-up}, and
 \ref{sec:low}, contain our alternative definitions of acceptability. 
 In Section \ref{sec:met} these definitions are integrated in  
 a methodology for proving termination.
  Finally, in
 Section \ref{sec:con}  some  conclusions are given. 
  This paper is an extended and revised
  version of \cite{mijcai95}.

\section{Preliminaries}\label{sec:pre}
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,\dots,s_k)$, or a  negated  atom  $\neg p(s_1,\dots,s_k)$, 
  or an  equality
 $s=t$,  or an  inequality  $\forall (s\not = t)$,  
 where   $\forall$ quantifies over some (perhaps none) of the variables
occurring in $s$, $t$. Equalities and inequalities are
  also called   {\em constraints}, and denoted by $c$.  
  An  inequality $\forall (s\not = t)$ is 
 {\em primitive} if it 
  is satisfiable but not valid. 
 For instance, $X\not=a$ is  primitive.  
  An    (extended) general logic {\em  program\/},
   denoted by $P$, $R$,
   is a finite set of 
   clauses  $$H\la L_1,\dots,L_m.$$ 
 with  $m\geq 0$,  where
 $H$ is an atom, and $L_i$ is a  literal, for $i\in[1,m]$.   
   A {\em query\/} is a finite 
  sequence  of literals, and is denoted by  $Q$. 
  


 To treat negated non-ground  atoms, Chan  (1988) proposes
  to augment 
 {\tt sld}-resolution with a procedure, informally described 
  as follows. For a substitution $\theta=\{X_1/t_1,\dots, X_n/t_n\}$,
  we denote  by $E_{\theta}$ the equality formula
  $(X_1=t_1\wedge \dots\wedge X_n=t_n)$.
   For any    negated atom $\neg A$, if 
  all the {\tt sld}-derivations of  $A$ are finite, and 
 $\theta_1$, $\dots , \theta_k$, with $k\geq 0$, are the 
 computed answer substitutions, then   
  the answers for $\neg A$ are obtained  from the
  negation of 
  $\exists (E_{\theta_1}\vee\dots\vee E_{\theta_k})$, 
where $\exists$ quantifies over 
  the variables   not occurring in $A$. 
 For instance, consider the program 
 \begin{program}
\> p(a) $\la$.\\
\> p(b) $\la$.
\end{program}
 The answer to the query $\neg p(X)$  is  $X\neq a\wedge X\neq b$.
 We call {\tt sldcnf}-resolution, 
    {\tt sld}-resolution  augmented with 
   Chan's procedure. 
 To show the correctness of {\tt sldcnf}-resolution, we choose as program
 semantics the
     Clark's completion \cite{cl78}. This semantics is a natural 
 interpretation of a {\sc 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,  $\forall$ quantifies
  over $X_1,\dots,X_k$. 
\begin{itemize}
\item  For every relation symbol $p$ occurring in $P$, having say   $k\geq 0$
 arguments:
 \begin{itemize}
\item  if $p$ does not occur in the head of any clause then
 add the formula 

$\forall  (p(X_1,\dots,X_k) \IFF {\em false})$;

\item   otherwise, if $k=0$ then add the formula 
 $p\IFF {\em true\/}$;  if $k>0$ and $C_1,\dots,C_l$, with  $l\geq 1$
 are all the  clauses of $P$ with head symbol $p$, with
  $C_i=p(s^i_1, \dots, s^i_k)\la Q_i$, then   add the formula
 $\forall   (p(X_1,\dots,X_k) \IFF
  \vee_{i\in [1,l]} ( \exists {\cal V}_i (E_i\wedge Q_i) )$, where
   ${\cal V}_i$ is the set of variables of  
  $C_i$,  $E_i$ is $(s^i_1=X_1\wedge \dots\wedge s^i_k=X_k)$,
  and  $X_1,\dots,X_k$ are fresh variables.
 \end{itemize}

\item   Finally, the following {\em free equality axioms\/} are added,  so that 
    the equality  theory of $comp(P)$ becomes 
    the  same as the one of the Herbrand universe. 
\begin{itemize}
 \item $f(X_1,\dots,X_k)=f(Y_1,\dots,Y_k) \rightarrow  
  (X_1=Y_1\wedge\dots\wedge X_k=Y_k)$, 

for every function symbol $f$,


 \item  $f(X_1,\dots,X_k)\neq g(Y_1,\dots,Y_m)$,

 for every distinct 
  function symbols
 $f$ and $g$,

\item  $X\neq s$,

   for every term $s$ s.t.\ $X$ occurs in $s$.
\end{itemize}
\end{itemize}


 The soundness of {\tt sldcnf}-resolution w.r.t.\
 Clark's  semantics follows 
 from 
  $$comp(P)\models \forall (A\leftrightarrow
 \exists (E_{\theta_1}\vee\dots\vee E_{\theta_k})),$$
 where $\forall$ quantifies over all the free variables of the formula.
     {\tt 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,    the notion of (infinite) derivation  
  is not  always defined. This is a problem for the study of
 termination
 of {\sc 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),
   where the subtrees  
  used to resolve negative literals 
   are built in a top-down way, constructing 
 their branches in parallel. 
  As a consequence,  the main derivation is  infinite if  
  at least one of these subtrees is infinite. 
 

 
  Termination of  {\sc glp\/}'s  depends on the selection rule.
 For instance, the program 
\begin{program}
\> p  $\la$ q,p. 
\end{program}
\NI terminates if the Prolog selection rule, which chooses
 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 programs containing  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 {\em Prolog selection rule\/}.
 An {\tt sldcnf}-tree that
  is obtained by using 
 the Prolog
 selection rule is called {\tt ldcnf}-tree. 




 
 To prove termination of  logic programs,  
    suitable functions from ground atoms to natural numbers,
   called level mappings, will be used. Let ${\cal B}_P$ denote the Herbrand
 base of $P$.
  
  
    
\begin{definition}{\tt (Level Mapping)}
A {\em level mapping} (for $P$) is a function $|\; |$ 
 from ${\cal B}_P$ 
to natural numbers.
\HB
\end{definition}

A level mapping is extended to negated ground atoms by  
  $|\neg A|=|A|$.
 We do not need to
 extend this notion also to constraints, because  they represent
  terminating   atomic 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. 

\section{Acyclic  Programs}\label{subsec:acy}
  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 \cite{m94},
   while acceptability will be discussed in Section \ref{subsec:acc}.
 
  Apt and Bezem (1991) study termination of {\sc glp\/}'s w.r.t.\ 
 an arbitrary selection rule. They   introduce 
 the following elegant syntactic  
  notion. 

\begin{definition}{\tt (Acyclic Program)}\label{acyclic}
A program $P$ is 
 {\em acyclic w.r.t.\ a level mapping} $|\; |$ if for
all ground instances $H\la L_1,\dots,L_n$ 
of clauses of $P$ we have that
 $|H|>|L_i|$
 holds 
 for all $i\leq 1\leq n$
  s.t.\ $L_i$ is not a constraint.  
   $P$ is   {\em acyclic} 
if there exists a level
mapping  $|\; |$ s.t.\  $P$ is  acyclic w.r.t.\ $|\; |$.
\HB

\end{definition}


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.  
  

\begin{definition}{\tt (Bounded Query)}\label{def:bq}
  Let $|\;|$ be a level mapping. A query $Q=L_1,\dots,L_n$ is  
 bounded (w.r.t.\ $|\; |$)  if    for every $1 \leq i\leq  n$,
 the set 
   $$|Q|_i=\{ |L_i'|\,\mid\, L'_i \mbox{ is a
 ground instance of $L_i$}\}$$ 
 is finite.
\HB 
  \end{definition}
 
 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. The converse of this result does not
 hold, due to the possibility of floundering.  Instead,
 using  Chan's constructive negation, we obtain a complete
 characterization \cite{m94}.

 First, we  
  formalize  the concept  of
 termination w.r.t.\ an arbitrary selection rule.
\begin{definition}{\tt (Terminating Query and Program)}
 A query is {\em  terminating} (w.r.t.\ $P$) if all its
 {\tt sldcnf}-derivations  (in $P$) are finite.
 A  program  $P$ is   {\em  terminating} 
 if  all   {\em ground\/} queries  are terminating w.r.t.\ $P$.
\HB
\end{definition}

\begin{theorem}\label{uno}
Let $P$ be an acyclic program and let $Q$ be a bounded query. 
Then every {\tt sldcnf}-tree for $Q$ in 
$P$
 contains only bounded queries and is finite.
\end{theorem}


 
 
\begin{theorem}\label{cinque}
Let $P$ be a terminating program. Then there exists a level
  mapping $|\; |$ s.t.: 
 {\bf (i)} $P$ is acyclic w.r.t.\  $|\; |$;
 {\bf (ii)} for every query  $Q$, $Q$ is bounded w.r.t.\ $|\; |$ iff
  $Q$ is terminating.
\end{theorem}

 From Theorems \ref{uno} and   \ref{cinque} it follows that
 terminating programs coincide with  acyclic programs
 and that for acyclic  programs 
 a query  has a finite {\tt sldcnf}-tree if and only if it is bounded.
 Notice that when negation as finite failure is 
 assumed, Theorem \ref{cinque}  does not hold.  For instance, 
 the program:
 \begin{program}
      \>   p(X) $\la$ $\neg$ q(Y).  \\
\> q(s(X)) $\la$ q(X).\\
 \> q(0) $\la$.
\end{program}
  is terminating (floundering) but it is not acyclic.\\


Finding a level mapping for proving acyclicity is a creative process.
 We refer the reader to   \cite{desde94} 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 implemented
  as an  acyclic program.

\subsection{An Example: Blocks World}\label{ex:2.1}
   The blocks world is a formulation of a   problem in AI, where
 a robot   performs 
 a number of primitive actions in a simple world 
 (see for instance Nilsson, 1982). 
  Here we consider a simpler 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
 initial situation by performing a sequence of possible moves.
 An example of an initial situation is given in Figure 1.
 

\Graphb{block.eps}{8cm}{Figure 1: The Blocks-World}

   Kowalski  (1979) gives a  clausal representation of 
 this problem    by means of pre- and post-conditions. 
 Here we  formulate the problem  using
  McCarthy and Hayes'
  situation calculus \cite{mcch69},  
  in terms of facts, events  and  situations. 
  There are three types of {\em facts}: $loc(X,L)$ 
  stands for  
    `block $X$ is in   location
 $L$'; ${\it above}(X,Y)$  for   
     `block $X$ is on   block $Y$'; and ${\it clear}(L)$
     for  
     `there is no block in    location $L$'.  
   There is  only one type of 
 {\em event}: ${\it move}(X,L)$ stands for
  `move  block $X$   into  location   $L$'.  Finally,  
 {\em situations}  are described using lists: $[\; ]$ denotes
 the initial  situation, and $[Xe|Xs]$    the situation obtained
 from $Xs$ by performing   the event
  $Xe$.
  Based on the above representation,
   the blocks world can be formalized as
   the following {\sc glp\/}  
 {\sc blocksworld\/}:


\begin{program}
\> $1)$ \ holds(l,[]) $\la.\mbox{ {\tt l}$\in {\cal L}$}$ \\
\> $2)$ \ block(bl) $\la.\mbox{ {\tt bl}$\in {\cal B}$}$ \\
\> $3)$ \ position(pl) $\la.\mbox{ {\tt pl}$\in {\cal P}$}$\\
\> $4)$ \ holds(loc(X,L),[move(X,L)|Xs]) $\la$\\
  \> \> \> block(X),\\
\> \> \> position(L),\\
\> \> \> holds(clear(top(X)),Xs),\\
\> \>  \> holds(clear(L),Xs), \\
\> \> \> L $\neq$ top(X). \\   
\> $5)$ \ holds(loc(X,L),[Xe|Xs]) $\la$ \\
\> \> \>  block(X),\\
\> \> \> position(L),\\
 \> \> \> $\neg$ abnormal(loc(X,L),Xe,Xs),\\
\> \> \> holds(loc(X,L),Xs). \\
\> $6)$ \ holds(above(X,Y),Xs) $\la$ \\
\> \> \> holds(loc(X,top(Y)),Xs).\\
\> $7)$ \ holds(above(X,Y),Xs) $\la$ \\
\> \> \> holds(loc(X,top(Z)),Xs),\\
   \> \>\> holds(loc(Z,top(Y)),Xs).\\
\> $8)$ \ holds(clear(L),Xs) $\la$ \\
\> \> \>  $\neg$ occupied(L,Xs). \\ 
\> $9)$ \ abnormal(loc(X,L),move(X,L'),Xs) $\la$. \\
\> $10)$  occupied(L,Xs)$\la$ \\
\> \> \>  holds(loc(X,L),Xs). \\
\> $11)$  legals([(a,L1),(b,L2),(c,L3)],Xs) $\la$\\
\> \> \>  holds(loc(a,L1),Xs),\\
\> \> \> holds(loc(b,L2),Xs), \\
\> \> \> holds(loc(c,L3),Xs).
  
\end{program}

 Here {\tt top(X)} denotes
  the top of   block {\tt X},  ${\cal B}=\{a,b,c\}$, 
  ${\cal P}=\{p,q,r,top(a),top(b),top(c)\}$, and
 ${\cal L}=\{loc(a,p),loc(b,q), loc(c,r)\}$.  Moreover,
   lines $1$, $2$ and $3$  abbreviate  
  sets of clauses, and line $1$ 
  specifies the initial situation.
  The  relation {\tt holds}   describes when  a fact is possible
   in a given  situation, and  the relation {\tt legals}
    when a   configuration is possible in a  given  situation.
 
 Consider the following level mapping, where for a ground term $y$,
    $|y|$ denotes  the length of the list $y$,  otherwise
   (i.e., if $y$ is not a list)
    $|y|$ is   $0$.\\
 
 $|block(x)|=0$, 

$|position(x)|=0$, 

$|abnormal(x,y,z)|=0$,


 $$|holds(x,y)|=  \left\{ \begin{array}{ll}
 3*|y|+1 & \mbox{if $x$ is  of the form ${\it loc}(r,s)$,} \hspace{4.75cm} \\
  3*|y|+3 & \mbox{if $x$ is  of the form ${\it clear}(r,s)$,}\\
  3*|y|+4 & \mbox{if $x$ is  of the form ${\it above}(r,s)$,}\\
  0 & \mbox{ otherwise.}
\end{array}
\right.$$

 $|occupied(x,y)|=3*|y|+2$,


$|legals(x,y)|=3*|y|+2$.\\

  

 It is easy to check that {\sc blocksworld\/} is acyclic w.r.t.\  
   $|\; |$.

  Therefore,  the class of questions expressed by means
 of bounded queries
   can be  completely answered. For instance,
      the question `when   block $a$  remains in its initial
 position $p$ under the occurrence of  an action?' can be
    formalized as  the query 
   {\tt holds(loc(a,p),[A])}.
  This query is bounded, hence   every of its 
 {\tt sldcnf}-derivations is finite, with answer
  $\forall L (A\neq move(a,L))$.

 Note that
 this query would flounder when  negation as finite failure  is used.

 
 
 


\section{Acceptable Programs}\label{subsec:acc}

In the previous section, we have seen
   how termination of  {\sc glp\/}'s w.r.t.\ an arbitrary selection rule can be
   proven by means of the notion of acyclicity.
  The notion of    acceptability   \cite{ap91} is used  for
 proving termination of {\sc glp\/}'s w.r.t.\ the Prolog selection rule.
  In this section, we  recall this notion, together with some
 useful results from \cite{m94}.
 Acyclicity and acceptability will be combined in the
  following sections to provide  more practical tools for
 proving termination of {\sc glp\/}'s w.r.t.\ the Prolog selection rule.


 In order to   study  termination
 of  general logic programs with respect to the Prolog selection 
 rule, Apt and Pedreschi   (1991) introduced
  the notion of   acceptable program.
  This notion is based on
  the  same condition used to define 
  acyclic programs, except that, for a ground instance 
 $H\la L_1,\dots, L_n$ of a clause, the 
   test  $|H| > |L_i|$ 
  is performed only  until the 
 first literal $L_{\overline{n}}$ which fails. This is sufficient  
 since, due to the Prolog selection rule,
 literals after $L_{\overline{n}}$ will not be selected. 
 To compute  $\overline{n}$, a
 class of  models of $P$, here called {\em \good models}, is used.
  The following notion is used. The
 {\em restriction} of an interpretation $I$ to a set $S$ 
  of relations, denoted by $I_{|S}$, is
 the set of   atoms of  $I$ having their relations   in $S$.
 
\begin{definition}{\tt (Specialized Model)}
  Let $Neg_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^-$ be the set of
 clauses in $P$   whose head contains a relation from $Neg_P$.
  Now a  model $I$ 
   of $P$ is {\em \good\/} if   $I_{|Neg_P}$ is a model of
$comp(P^-)$.
\HB

\end{definition}
 
   

\begin{definition}{\tt (Acceptable Program)}\label{acp}
 Let $|\; |$ be a level mapping for $P$ and let $I$ be 
 an interpretation  of $P$.
   $P$ is   {\em acceptable  w.r.t.\ $|\; |$ and $I$} if 
 $I$ is a \good model of $P$, and for
all ground instances $H\la L_1,\dots,L_n$ of clauses of $P$ 
we have that $|H|>|L_i|$
 holds 
 for every
$1\leq i\leq \overline{n}$ s.t.\ $L_i$ is not a constraint, where 
$\overline{n} =min (\{ n\}\cup \{i\in [1,n]\; | \; I\not\models
 L_i\})$.
    $P$ is   {\em acceptable} if it is acceptable w.r.t.\ some  level
mapping   and interpretation.
\HB
 
\end{definition}
 If a program is acceptable, then
 every ground query has only finite {\tt 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. 
   
 

\begin{definition}{\tt (Bounded Query)}
 Let $|\; |$ be a 
 level mapping  and let $I$  be 
a  \good  model  of $P$. 
 A query  $Q= L_1,\dots,L_n$  is bounded (w.r.t.\
  $|\; |$   and  $I$)  if  
  for every $1\leq i \leq n$ 
$$\begin{array}{lll}
 |Q|^i_I=& \{ |L_i'|\,\mid \, & \mbox{$L'_1,\dots,L_i'$ ground instance
  of $L_1,\dots,L_i$ and}
\\
 &  &\mbox{$I\models L'_1,\dots,L'_{i-1}$}\}
\end{array}$$
is finite.
\HB
\end{definition}



 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 \cite{m94}. 
   First, we  formalize  the concept of termination w.r.t.\ the Prolog
  selection rule.
 
\begin{definition} {\tt (Left-Terminating Query and Program)} 
 A query is  
  {\em left-terminating\/} \, \,   (w.r.t.  $P$) if all its
 {\tt ldcnf}-derivations 
   are finite.
A program $P$ is    {\em left-terminating}
  if  every  ground query is left-terminating w.r.t.\ $P$.
\HB
\end{definition}
 
\begin{theorem}\label{acc-1}
Let $P$ be an acceptable program and let $Q$ be a bounded query.
  Then every {\tt ldcnf}-tree for $Q$ in $P$  contains only bounded
queries and is finite.
\end{theorem}

 

\begin{theorem}\label{acc-5}
Let $P$ be a left-terminating program. Then there exists
 a level
  mapping $|\; |$, and  a \good model $I$ of $P$ s.t.: 
{\bf (i)} $P$ is acceptable w.r.t.\  $|\; |$ and $I$;
 {\bf (ii)} for every query $Q$, $Q$ is bounded w.r.t.\ $|\; |$  
and $I$ 
 iff $Q$ is left-terminating.
\end{theorem}
 In the following section   an
   acceptable program that formalizes  planning in the  blocks world
is given.

\subsection{An Example: Planning in the Blocks World}\label{ex:2.2}
 Consider     planning  in the
  blocks world,  amounting to  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  \cite{ss94}: {\em while the desired configuration
  has not yet been  reached,
 find a legal action, update the current configuration, and check
 that it was not   already obtained.}  
  The    following  program {\sc planning\/} 
 follows this approach: it consists of all the clauses
 of the program {\sc blocksworld\/}, minus 6) and 7), and
   plus the following clauses:
 
 \Graphb{plan-block.eps}{15cm}{Figure 2: Planning in the Blocks-World}
 

 
\begin{program}
\> $1p)$ \ transform(Xs,St,Plan) $\la$ \\
 \> \> \>  state(St0),\\
\> \> \>  legals(St0,Xs), \\
\> \> \>  trans(Xs,St,[St0],Plan).
\\
\> $2p)$ \ trans(Xs,St,Vis,[ ]) $\la$ \\
\> \> \>  legals(St,Xs). \\
\> $3p)$ \ trans(Xs,St,Vis,[Act|Acts])  $\la$ \\
\> \> \>  state(St1), \\
\> \> \>  $\neg$ member(St1,Vis),\\
 \> \> \>   legals(St1,[Act|Xs]), \\
\> \>  \>   trans([Act|Xs],St,[St1|Vis],Acts).\\
\> $4p)$ \ state([(a,L1),(b,L2),(c,L3)]) $\la$ \\
\> \> \>  P=[p,q,r,top(a),top(b),top(c)],\\
\> \> \>   member(L1,P), \\
\> \>  \>  member(L2,P), \\
\> \> \>  member(L3,P).
\\
\> $5p)$ \ member(X,[X|Y]) $\la$. \\
\> $6p)$ \ member(X,[Y|Z]) $\la$  \\
\> \>  \>   member(X,Z). \\
\end{program}
  Planning in the blocks-world is specified by the relation
  {\tt transform}: in clause    $1p)$ first     a legal configuration
  for the actual situation is found by means of the predicate
 {\tt legals};   then  
   the predicate {\tt trans} is used to
   construct incrementally a 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   termination  of the construction
  when  the  final configuration is reached. 
 


 To prove the acceptability of {\sc planning\/},  
  we have to find a model of  {\sc planning\/}  that is also a 
 model of $comp(\{5p), 6p)\}\cup$
  {\sc blocksworld}$\setminus \{ 6), 7), 11)\})$.
 We do not need to use all this semantic information,
 because     from the acyclicity of  {\sc blocksworld},
   it follows that {\sc planning\/}  is left-terminating   if
   the following program  {\sc tras\/} is acceptable. 
    We postpone the justification
  of    this claim till the next section.
   
 \begin{program}
\> $1'p)$ \ transform(Xs,St,Plan) $\la$  \\
   \> \> \> state(St0),\\
 \> \> \>  trans(Xs,St,[St0],Plan).\\
\> $2p)$ \ trans(Xs,St,Vis,[ ]) $\la$. \\
\> $3'p)$ \ trans(Xs,St,Vis,[Act|Acts])  
$\la$ \\
 \> \> \> state(St1),\\
  \> \> \> $\neg$ member(St1,Vis),  \\
      \> \>  \> trans([Act|Xs],St,[St1|Vis],Acts).\\
\> $4p)$ \ state([(a,L1),(b,L2),(c,L3)]) $\la$\\
 \> \> \> P=[p,q,r,top(a),top(b),top(c)],\\
\> \> \> member(L1,P),\\
 \> \> \> member(L2,P),\\
 \> \> \> member(L3,P).\\
\> $5p)$ \ member(X,[X|Y]) $\la$. \\
\> $6p)$ \ member(X,[Y|Z]) $\la$\\
 \> \>  \>  member(X,Z). \\
\end{program}
 {\sc tras\/} is obtained from
     {\sc planning\/}  by first
 deleting  the subprogram `defining'  {\tt  legals},
 and next   the literals  with relation {\tt  legals} occurring
 in the body of the remaining clauses.
  By considering {\sc tras\/}, we  need  less semantic information,
 namely   a model of {\sc tras\/} that is also
 a model of $comp(\{ 5p), 6)\})$.
  To show that {\sc tras\/} is acceptable, we consider the following
   level mapping:\\


 
 $|member(x,y)|=|y|$;

 $|state(x)|=7$;

 $|trans(x,y,z,w)|= tot- card(el(z)\cap S)+ 3*(|x|+1) +5 +|z|$;


 $|transform(x,y,z)|= tot+3*(|x|+1) +6$.\\


\NI  Above,   $S$ denotes $ \{ [(a,p1),(b,p2),(c,p3)]\, \mid 
  \mbox{   $\{p1, p2, p3 \}\subset 
   \{p,q,r,top(a),top(b),top(c)\}$}\}$,
   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)\cap S)$  is
  the cardinality
 of the set $el(z)\cap S$; finally, if $x$ is a list then $|x|$ denotes 
 its length, otherwise it denotes   $0$.
 Observe that $( tot- card(el(z)\cap S))\geq 0$.
 Thus $|\; |$ is well defined.  
  For an atom  $p(s_1,\dots,s_n)$, we denote by
  $[p(s_1,\dots,s_n)]$  the set of all its  ground instances.
 Consider the following 
  interpretation
   $I=I_{transform}\cup I_{trans}\cup I_{member}\cup
 I_{state}$ of  {\sc tras\/}, with: \\

  $I_{transform}= [transform(X,Y,Z)]$,

 $I_{trans}= [trans(X,Y,Z,W)]$,

 $I_{member}= \{member(x,y)\, \mid\, \mbox{$y$ is a list 
 s.t.\  $x\in set(y)$}\}$, 

 $I_{state}=  
 \{ state(x)\, \mid \, x\in S\}$.  \\
 

    It is easy to prove that $I$ is a model of
  {\sc tras\/}.   
 Moreover,   $Neg_{tras}=\{ member \}$,
   and {\sc tras\/}$^-$ is equal to
  $\{5p), 6p)\}$. So,  $I_{|\{member\}}$  
  is a model of $comp(${\sc tras\/}$^-)$. 
  To show that   {\sc tras\/}
  is acceptable w.r.t.\ $I$ and $|\; |$, we use    the following
   properties of $|\; |$,  which are readily verified: 

\begin{equation}\label{pl-1}
 |transform(x,y,z)|_1\geq 8,
\end{equation}
\begin{equation}\label{pl-2}
 |trans(x,y,z,w)|_1\geq 8,
\end{equation} 
\begin{equation}\label{pl-3}
 |trans(x,y,z,w)|_1> |z|.
\end{equation}

 
The proof of the acceptability of {\sc tras\/} proceeds as follows:
\begin{itemize}

\item  Consider a ground instance: 

 $transform(xs,xt,plan) \la  state(st0),    trans(xs,st,[st0],plan).$

\NI of $1p)$. From (\ref{pl-1}) it follows that: 

$$|transform(xs,xt,plan)| > |state(st0)|.$$

  Suppose that $I\models  state(st0)$. Then  $st0\in S$, so
 $card(el(S\cap el([st0]))= 1$; hence:

$$|transform(xs,xt,plan)| > |trans(xs,st,[st0],plan)|.$$

\item  Consider a ground instance: 
 

 $ trans(xs,st,vis,[act|acts])  \la$

$\qquad \qquad state(st1), \neg member(st1,vis),  
        trans([act|xs],st,[st1|vis],acts).$
 

\NI of $2'p)$.  From (\ref{pl-2}) it follows that: 

$$|trans(xs,st,vis,[act|acts])| > |state(st1)|,$$

\NI  and from (\ref{pl-3}): 

$$|trans(xs,st,vis,[act|acts])| > |\neg member(st1,vis)|.$$


 Suppose that $I\models  state(st1), \neg member(st1,vis)$.
 Then  $st1\in S$, but $st1\not\in set(vis)$; so
 $card( S\cap el([st1|vis]))= card( S\cap el(vis))+1$; 
 hence  $tot - card( S\cap el([st1|vis]))< tot-card( S\cap el(vis))$.
  Therefore,

$$|trans(xs,st,vis,[act|acts])| > 
|trans([act|xs],st,[st1|vis],acts) |.$$

\item  The proof for the  other clauses of {\sc tras\/}
  is similar.
\end{itemize}
 



\section{Up-Acceptability}\label{sec:up}
  
 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 {\sc glp\/}'s.  

  In Section \ref{ex:2.2}  we claim that in order to prove left-termination
 of {\sc planning\/}, it is sufficient to prove acceptability
 of  the `part' of {\sc planning\/}  called {\sc tras\/} and acyclicity of
  the rest of the program. Let us explain how we arrive to this conclusion.
 First, {\sc planning\/} is partitioned into two parts: an upper part, say $P_1$ consisting of
 clauses $1),\dots,6)$, and a lower part, say $R$, consisting
 of the rest of {\sc 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 {\em relation\/}    is   {\em defined in $P$\/} if it occurs
 in the head of at least one of its clauses, and that
  a  {\em literal\/} is  {\em defined in $P$\/} 
 if its relation 
 is  defined in $P$.

\begin{definition}{\tt (Program Extension)}\label{ut}
  A program {\em $P$ extends a program $R$}, denoted by $P > R$,
 if  no relation defined in  $P$ occurs in $R$.
\HB
 \end{definition}

  So $P$ extends $R$ if $P$ defines  new relations  
 possibly using the relations defined already in $R$.
 For instance, the program  $P_2$:
  \begin{program} 
 \> p $\la$   q,r.
 \end{program}
  extends the program  $P_1$:
\begin{program} 
 \> q $\la$ s.\\
\> s $\la$.
\end{program}
 
 Next, we consider  the program {\sc tras\/} obtained from $P_1$
 by deleting all the literals defined in $R$. We call
 this operation {\em difference}, defined as follows.
  
\begin{definition}{\tt (Difference of Two Programs)}\label{def:diff}
 The {\em difference of the programs $P$ and   $R$},
 denoted by     $P\setminusp R$, is    the 
 program obtained from $P$ by deleting all the clauses of $R$ 
 and all the literals defined in  $R$. 
\HB
 \end{definition}
 For instance,
 if $P_1$ and $P_2$ are defined as above, then  $P_2\setminusp P_1$ is  
 the program {\tt p$\la$ r\/}.

Finally, we prove  that {\sc tras\/} is acceptable and that $R$ is acyclic, 
 and in doing that we  have to  take care that
 the two level mappings  used are related by a condition, namely
 that for every ground instance, say $C=H\la 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$
\begin{program}
$1)$  q(f(X)) $\la$ p(Y), q(X).\\
 $2)$  p(f(X)) $\la$ p(X).
\end{program}

\NI and take $P_1=\{1)\}$ and $R=\{2)\}$. Then $P_1$ extends $R$, $P_1\setminusp R$
 is acceptable w.r.t.\ the level mapping $|q(x)|_{P_1}=|x|$,
 $R$ is acyclic w.r.t.\  the level mapping $|p(x)|_{R}=|x|$,
 but $P$ is not left-terminating.


So, the  steps we applied to {\sc planning\/} are summarized in the following
 definition of up-acceptability, that  characterizes left-terminating
 programs.


  For a level mapping $|\;|$ and a program $R$,  
 the {\em restriction of $|\;|$    to    $R$\/},
    denoted $|\;|_{|R}$, is the level mapping
 for $R$ defined by $|A|_{|R}=|A|$.

\begin{definition}{\tt (Up-Acceptability)}\label{e-acc}
 Let $|\;|$ be a level mapping for $P$. Let $R$ be  
  s.t.\ $P=P_1\cup R$ for some $P_1$, and
 let $I$ be an interpretation of $P\setminusp R$.
   $P$ is   {\em up-acceptable w.r.t.\ $|\;|$, 
      $R$ and $I$\/} if the following conditions hold:
\begin{enumerate}
 \item    $P_1$   extends $R$;
   \item   $P\setminusp R$ is acceptable w.r.t.\  
  $|\; |_{|P\setminusp R}$ and $I$;
  \item $R$ is acyclic w.r.t.\    $|\; |_{|R}$;
   \item  for every ground instance $H\la L_1,\dots,L_n$ 
 of a clause of $P_1$, for every $1\leq i\leq n$,
\begin{itemize}
 \item  if  $L_i$  is defined in $R$  
 and is not a constraint, and
 \item if   $I\models L_{i1},\dots,L_{ik}$, where 
 $L_{i1},\dots,L_{ik}$
 are those literals among $L_1,\dots,L_i$ whose relations occur in
 $P\setminusp R$, 
\end{itemize}
  then  $|H|\geq |L_i|$.
\end{enumerate}
 A program is    {\em up-acceptable\/} if there exist  $|\;|$,
  $R$  and $I$ s.t.\
 $P$ is up-acceptable 
 w.r.t.\  $|\;|$,
  $R$, $I$.

\HB
\end{definition}


 Observe that by taking for $R$   the empty set of clauses,
 we obtain the original definition of acceptability.
 Next,   we introduce the notion of {\em up-bounded query}.

\begin{definition}{\tt (Up-bounded Query)}
  Let $P$ be   up-acceptable w.r.t.\ $|\; |$,
    $R$ and $I$, and let  $Q=L_1,\dots,L_n$. 
   $Q$ is   up-bounded if for every $1\leq i\leq n$ the set
  $$|Q|^{up,I}_i =\{ |L'_i|\,\mid\, L'_1,\dots,L'_n \mbox{ is a ground instance
 of $Q$ and $I \models L'_{k_1}\wedge\dots\wedge L'_{k_{l}}$}\}$$
  is finite, where $L'_{k_1},\dots, L'_{k_{l}}$ are the literals of 
 $ L'_1,\dots,L'_{i-1}$  whose relations occur in $P\setminusp R$.

\HB
 \end{definition}
   



 In order to show that all  {\tt ldcnf}-derivations of an
 up-bounded query are finite:   
 we shall prove that a {\tt 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 {\em multiset} (see e.g.,\ Deshowitz, 1987) is a
  unordered collection
 in which the number of occurrences of each element is counted. 
  Formally, a multiset of natural numbers is a function from
  the set   ($N$, $<$) of natural numbers to itself,
  giving the multiplicity
 of each natural number. 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 smaller under $<$. Since  $<$ is well-founded,
 the induced ordering $<_{mul}$  is also well-founded.
 For simplicity we shall omit in the sequel the subscript {\em mul}
 from $<_{mul}$.

 With an up-bounded query $Q$, we associate a pair 
 $\pi(Q)_{up,I}=(|[Q]|_{up,I,P_1}, |[Q]|_{up,I,R})$ of    multisets,
  where for a program $P$ and an interpretation $I$
 $$|[Q]|_{up,I,P}=bag( max |Q|^{up,I}_{k_1},\dots , 
 max |Q|^{up,I}_{k_m}),$$ 
  where $L_{k_1},\dots,L_{k_m}$ are those literals
  of $Q$  whose relations occur in  $P\setminusp R$,
  and  $max |Q|^{up,I}_i$ is the maximum
 of  $|Q|^{up,I}_i$ (which is by convention  $0$
 if $|Q|^{up,I}_i$ is the empty set). 
 
 Recall that the lexicographic order $\prec$
  (on pairs of   multisets)     is 
 defined by  $(X,Y)\prec (Z,W)$ iff either $X<  Z$, or $X=Z$
 and $Y<  W$.

     Then we can prove the   following result.

\begin{theorem}\label{mod}
 Suppose that $P$ is up-acceptable w.r.t.\ $|\;|$,  $R$ and $I$.
 Let $Q$ be an up-bounded query. Then every
  {\tt ldcnf}-derivation for $Q$ in   $P$ contains only up-bounded
 queries and is finite. 
\end{theorem}
\Proof  
 Let $\xi=Q_1,\dots,Q_n,\dots$ be a {\tt 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_{n-1}$ 
  by the selection of a    literal which is not a constraint,
   then  $ \pi(Q_n)_{up,I} <  \pi(Q_{n-1})_{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-1$.  Thus, $Q_{n-1}$ is up-bounded.   Suppose that 
  the resolvent of $Q_{n-1}$ is defined
 and that the selected literal, say $L$, is not a constraint.
    It follows
  from the fact that $Q_{n-1}$ 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  $\pi(Q_{n})_{up,I}$ is   smaller 
 than $\pi(Q_{n-1})_{up,I}$ 
  in the lexicographic order. If  the relation symbol 
    of $L$ occurs in $P\setminusp R$ then the
  first component of   $\pi(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   $\pi(Q_{n})_{up,I}$ does not 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.
\HB
\VV

\begin{example}{\tt ({\sc planning\/} is Up-Acceptable)}\label{ex:plup}
   Call R-{\sc blocksworld} the program obtained from
 {\sc blocksworld} by deleting the clauses
   $6)$ and $7)$.
    We prove that {\sc planning\/}  is up-acceptable w.r.t.\   $|\; |$,
  R-{\sc blocksworld}, and $I$ defined as in the examples
 of Sections  \ref{ex:2.1}
 and \ref{ex:2.2}.  
  {\sc planning\/}$\setminusp$R-{\sc blocksworld}  is (not incidentally)
 the program  {\sc tras\/}. The proof of up-acceptability proceeds as follows.
 \begin{enumerate}
\item  {\sc planning\/} extends R-{\sc blocksworld}.
\item   It  is  proven   in Section
 \ref{ex:2.2} that {\sc tras\/} is  acceptable.
\item    It   is  proven 
     in Section \ref{ex:2.1} that R-{\sc blocksworld}     acyclic. 
\item 
 Consider a ground instance

 $transform(c,s,p) \la state(s0), legals(s0,c),trans(c,s,[s0],p).$

\NI of $1)$, and suppose that $I\models state(s0)$. Then

  $|transform(c,s,p)|=tot+3*(|c|+1)+6\geq 3*|c|+2= |legals(s0,c)|$.

 Consider a ground instance

 $trans(c,s,v,[\; ]) \la  legals(s,c).$

\NI of $1)$. Then 

 
$|trans(c,s,v,[\; ])|=tot-card(el(v)\cap S)+3*(|c|+1)+5+|v|\geq 3*|c|+2 $.



\end{enumerate}
 
\HB
\end{example}

The following corollary establishes  the equivalence
 of the notions of acceptability and up-acceptability.
 It follows directly from   Theorem \ref{mod}  and  Theorem 
 \ref{acc-5}.

\begin{corollary}\label{equi}
 A   general  logic program   is up-acceptable  if and only if it is acceptable.
\end{corollary}

\section{Weak Up-Acceptability}\label{sec:weakly-up}
    Because  in 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.

\subsection{An Example: Hamiltonian Path}\label{ex:hamil}
 A  Hamiltonian path  of a graph  is an acyclic path 
   containing  all the nodes of the graph.
  The following   program {\sc hamiltonian\/} defines hamiltonian
 paths: it consists of the following clauses
 \begin{program}
\> $1)$ ham(G,P) $\la$  \\
 \> \>  \> path(N1,N2,G,P),\\
 \> \> \> cov(P,G). \\
\> $2)$ cov(P,G) $\la$\\
\> \>  \>  $\neg$ notcov(P,G).\\
 \> $3)$ notcov(P,G) $\la$\\
\> \> \>    node(X,G), $\neg$ member(X,P).\\
 \> $4)$ node(X,G) $\la$\\
\> \>  \>   member([X,Y],G).\\
 \> $5)$ node(X,G) $\la$\\
  \> \> \>   member([Y,X],G).\\
\end{program}
augmented with the program {\sc acypath\/}  defining acyclic paths:
  
\begin{program}
\> $p1)$  path(N1,N2,G,P) $\la$ \\
\> \> \> path1(N1,[N2],G,P).\\
\> $p2)$ path1(N1,[N1|P1],G,[N1|P1]) $\la$. \\
\> $p3)$ path1(N1,[X1|P1],G,P) $\la$\\
\> \> \> member([Y1,X1],G),\\
\> \>  \>  $\neg$ member(Y1,[X1|P1]), \\
\> \>  \>  path1(N1,[Y1,X1|P1],G,P).\\
\> $p4)$  member(X,[X|Y]) $\la$. \\
\> $p5)$  member(X,[Y|Z]) $\la$ \\
\> \> \>  member(X,Z). 
\end{program}
 
 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,\bot]]$, where 
 $\bot$ 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 $[x|p1]$ is 
 transformed into $[y,x|p1]$ if   there is an edge $[y,x]$ in the graph
  $g$ such that $y$ is not 
 already present in $[x|p1]$. The construction terminates if
 $y$ is equal 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 acyclic path
 of $g$ that covers all its nodes.  The relation $cov$
 is defined   as the negation of 
    $notcov$, where  
  $notcov(p,g)$ is true  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,  
  {\tt ham([[a,b],[b,c],[a,a],[c,b]], [a,b,c])} holds, corresponding
 to the path  drawn in bold  in the graph of Figure 3.


\Graphb{ham.eps}{8cm}{Figure 3: The  Hamiltonian path of 
$[[a,b],[b,c],[a,a],[c,b]]$}
 

   The program  {\sc hamiltonian\/} 
   is not terminating, because {\sc acypath\/} is not.
   However, {\sc hamiltonian\/}   
   is left-terminating.  In order to prove this result
   using  acceptability (Definition \ref{acp}), we need   
   to find a   model of {\sc hamiltonian\/}   that is also
 a model of  the completion  
  $comp(\{ 3), 4),  5), p4) ,p5)\})$ 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  {\sc hamiltonian\/}   in two subprograms:   
   $P_2$ consisting of    {\sc acypath\/}  plus clause 1), and    $P_1$
  consisting of the remaining clauses $2)-5)$.
   Note that $P_2$ `almost' extends $P_1$, because $P_1$ contains
  some literals (those with relation $\{member\}$) 
     defined in $P_2$. Since the subprogram $5p),6p)$ 
  defining these literals is extended by both  $P_1$ and
    by $P_2\setminus\{5p),6p)\}$,  it follows that
   left-termination of   $\{5p),6p)\}$  does not depend
  on the termination behaviour of the rest of  {\sc hamiltonian\/}.
   So, for proving left-termination of {\sc hamiltonian\/}  it is
  sufficient to  show that $P_2\setminusp P_1$ is acceptable,  
  that $P_1$ is acyclic, and that the  corresponding 
  level mappings  satisfy the condition in 
   Definition \ref{e-acc}. Thus, we need only to find a  
 model of $P_2\setminusp P_1$ that is also
 a model of  $comp(\{ p4) ,p5)\})$.
   \HB


   
    

\subsection{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_{|S}$ denotes  the clauses of $P$
  that  define the relations from $S$.   

\begin{definition}{\tt (Program Weak Extension)}\label{wex}
  A program {\em $P$ weakly extends a program $R$}, 
  denoted by $P >_w R$,
 if for some set $S$ of relations we have that:
\begin{itemize}
\item $P=P_1\cup P_{|S}$, and $P_1$ extends $ P_{|S}$;
\item $R$ extends $ P_{|S}$; and
\item $P\setminusp P_{|S}$ extends $R\setminusp P_{|S}$.
 \HB
\end{itemize}  
\end{definition}

 Note that only the relations of $S$ which are defined in $P$ play
 a role in the above definition.  
   Definition \ref{ut} is a particular case of the above
 definition,   obtained by considering $P_{|S}$ to be equal to
 $\emptyset$ (which includes the case that $S=\emptyset$).

\begin{example}
 The program
 \begin{program}
\> p(X) $\la$  q(X), r(X).\\ 
\> r(f(X)) $\la$ r(X).
\end{program}

\NI weakly extends the program
 \begin{program}
\> q(X) $\la$  s(X), r(X).\\ 
\> s(X) $\la$.
\end{program}
  This can be seen by taking $S=\{ r\}$. Then $P_1$ is {\tt p(X) $\la$  q(X), r(X).},
  $P_{|S}$ is {\tt  r(f(X)) $\la$ r(X).}, $P_1$ and $R$ both
 extend  $P_{|S}$.  Moreover,  $P\setminusp P_{|S}$ is
 {\tt  p(X) $\la$  q(X).} and $R\setminusp P_{|S}$ is 
 \begin{program}
\> q(X) $\la$  s(X).\\ 
\> s(X) $\la$.
\end{program}
 Finally,  it is easy to check that  $P\setminusp P_{|S}$ extends 
  $R\setminusp P_{|S}$.
 \HB
\end{example}


Thus the notion of weak  up-acceptability 
   is obtained from Definition \ref{e-acc} by replacing
 in condition 1   `extends' by  
 `weakly extends'.
 
\begin{definition}{\tt (Weak  Up-Acceptability)}\label{def:wup}
 Let $|\;|$ be a level mapping for $P$. Let $R$ be a set
 of clauses   s.t.\ $P=P_1\cup R$ for some $P_1$, and
 let $I$ be an interpretation of $P\setminusp R$.
   $P$ is  {\em weakly up-acceptable w.r.t.\ $|\;|$, 
      $R$ and $I$\/} if the following conditions hold:
\begin{enumerate}
 \item    $P_1$  weakly  extends $R$;
   \item  $P\setminusp R$ is acceptable w.r.t.\  
  $|\; |_{|P\setminusp R}$ and $I$;
  \item $R$ is acyclic w.r.t.\    $|\; |_{|R}$;
   \item  for every ground instance $H\la L_1,\dots,L_n$ 
 of a clause of $P_1$, for every $1\leq i\leq n$,
\begin{itemize}
 \item  if $L_i$ is defined in $R$  
 and is not a constraint, and
 \item if   $I\models L_{i1},\dots,L_{ik}$, where 
 $L_{i1},\dots,L_{ik}$
 are those literals among $L_1,\dots,L_i$ whose relations occur in 
 $P\setminusp R$, 
\end{itemize}
  then  $|H|\geq |L_i|$.
\HB
\end{enumerate}
\end{definition}

In order to prove  the analog to    Theorem \ref{mod},
   we need to use triples of finite multisets, instead of pairs,
  with the lexicographic ordering  $\prec$: 
    $(X_1,X_2,X_3)\prec (Y_1,Y_2,Y_3)$ iff either 
 $(X_1,X_2)\prec  (Y_1,Y_2)$ (by abuse of notation
  we use $\prec$ also to denote  the lexicographic ordering 
 on pairs of   multisets), 
   or   $X_1=Y_1$ and
 and $X_2=  Y_2$ and $X_3<Y_3$.
  We consider the triple:
  $$\tau(Q)_{up,I}=(|[Q]|_{up,I,P\setminusp P_{|S}},
 |[Q]|_{up,I,R\setminusp P_{|S}}, 
 |[Q]|_{up,I,P_{|S}}).$$ 
 

 
 
\begin{theorem}\label{w-mod}
 Suppose that $P$ is weakly  up-acceptable w.r.t.\ $|\;|$,  $R$ 
  and $I$.
 Let $Q$ be an up-bounded query. Then every
  {\tt ldcnf}-derivation for $Q$ in   $P$ contains only up-bounded
 queries and is finite. 
\end{theorem}
\Proof  
 Let $S$ be the set of relations used to prove that
  $P$ is weakly  up-acceptable w.r.t.\ $|\;|$,  $R$ 
  and $I$. 
 The proof is similar to the one of Theorem \ref{mod},   except
 that  we consider   $ \tau(Q)_{up,I}$ instead of   $ \pi(Q)_{up,I}$,
 and  we show that  $\tau(Q_{n})_{up,I}$ is   smaller 
 than $\tau(Q_{n-1})_{up,I}$ 
  in the lexicographic order as follows.
  If the relation symbol of  $L$ occur in $P\setminusp R$ 
  but not in $S$,
 then the
  first component of   $\tau(Q_{n})_{up,I}$ becomes smaller 
 because of condition 2.
 Otherwise, if the relation symbol of  $L$ occur in $R$ then 
 the first component of   $\tau(Q_{n})_{up,I}$ does not increase
 because of   condition 1, while the second one becomes
 smaller because of condition 3. Finally, if the relation symbol 
 of  $L$ occur in 
 $S$, 
 then 
 the first and second components of 
   $\tau(Q_{n})_{up,I}$ do  not increase, because of   condition  1, 
 while the third one becomes
 smaller because of condition 2. 
\HB
\VV
  
\begin{example}{\tt ({\sc hamiltonian\/}  is Weakly Up-Acceptable)}
\label{ex:weak-up}
  We prove  that  {\sc hamiltonian\/}   is   weakly  up-acceptable.
  Consider as upper part   
 the program  $P_2$ consisting of {\sc acypath\/}  augmented with clause 1),
 and as lower part the program $P_1$:
 \begin{program}
\> $2)$ cov(P,G) $\la$\\
\> \>  \>  $\neg$ notcov(P,G).\\
 \> $3)$ notcov(P,G) $\la$\\
\> \>  \>   node(X,G), $\neg$ member(X,P).\\
 \> $4)$ node(X,G) $\la$\\
\> \>  \>   member([X,Y],G).\\
 \> $5)$ node(X,G) $\la$\\
  \> \>   \> member([Y,X],G).\\
\end{program}


 Take  $\{member\}$ as set $S$ 
 of relations. 

\begin{enumerate}
\item    $P_2$  weakly extends $P_1$.

\item  The program $P_2\setminusp P_1$, consisting of

 \begin{program}
\> $1)$ ham(G,P) $\la$  \\
 \> \> \> path(N1,N2,G,P). \\
\> $p1)$  path(N1,N2,G,P) $\la$ \\
\> \> \> path1(N1,[N2],G,P).\\
\> $p2)$ path1(N1,[N1|P1],G,[N1|P1]) $\la$. \\
\> $p3)$ path1(N1,[X1|P1],G,P) $\la$\\
\> \> \> member([Y1,X1],G),\\
\> \>  \>  $\neg$ member(Y1,[X1|P1]), \\
\> \>  \>  path1(N1,[Y1,X1|P1],G,P).\\
\> $p4)$  member(X,[X|Y]) $\la$. \\
\> $p5)$  member(X,[Y|Z]) $\la$ \\
\> \> \>  member(X,Z). 
\end{program}

\NI  is acceptable w.r.t.\ the following level mapping:

 $|member(s,t)|= |t|$;

$|path1(n1,p1,g,p)|= |p1| + |g|+ 2(|g| - |p1\cap g|) +1$;

$|path(n1,n2,g,p)| =  3|g|+3$;

$|ham(g,p)| =  3|g|+4$,

and the interpretation
 $I= I_{ham}\cup I_{path}\cup I_{path1}\cup I_{member}$,
   with:

$I_{ham}= [ham(G,P)]$,

$I_{path}=\{path(n1,n2,g,p) \, \mid\,  |g|+1 \geq |p| \}$,

$I_{path1}=\{ path1(n1,p1,g,p)\,\mid\, |p1|- |p1\cap g| 
 \geq |p|- |p\cap g|\}$,

$I_{member}= \{member(s,t)\, \mid\, \mbox{$t$ list s.t.\  $s\in set(t)$}\}$,

 where for two lists  $p$ and $g$,
  $p\cap g$ denotes  the list containing as elements
 those $x$  which are elements of  $p$ for which there
 exists a $y$ s.t.\ $[x,y]$ is an element of  $g$. 


 We prove that
   $I$ is a model of $P_2$.

 \begin{itemize}
\item  Consider a ground instance of the clause p1) and 
 suppose that $$I\models path1(n1,[n2],g,p).$$ Note that
 $|[n2]|- |[n2]\cap g|\leq 1$. So  $|p|-|p\cap g|\leq 1$.
 But $|p\cap g|\leq |g|$. Then $|p|\leq |g|+1$,
  hence $I\models path(n1,n2,g,p)$.
 \item  Consider  a ground instance of the clause p3) and suppose that
 $$I\models member([y1,x1],g),\neg member(y1,[x1|p1]), 
 path1(n1,[y1,x1|p1], g,p).$$ 

 Thus $|[y1,x1|p1]|- |[y1,x1|p1]\cap g|\geq |p|-|p\cap g|$, where
 $y1\not\in [x1|p1]$ and $[y1,x1]\in g$. Therefore
 $|[y1,x1|p1]\cap g|= 1+ |[x1|p1]\cap g|$. 
 So $|[y1,x1|p1]|- |[y1,x1|p1]\cap g|= |[x1|p1]| - |[x1|p1]\cap g|$.
 Then $|[x1|p1]| - |[x1|p1]\cap g| \geq |p|-|p\cap g|$. Hence 
 $I\models path1(n1, [x1|p1], g, p)$.

\item The proof   for the other clauses is analogous.
\end{itemize}
 Now, $Neg_{P_2}=\{member\}$ and $P_2^-=\{ (f), (g)\}$.
 It is routine  to check that
  $I_{|\{member\}}$  is a model of $comp(P_2^-)$.

\item   $P_1$ is acyclic w.r.t.\ the level mapping:

 $|cov(p,g)|=|p|+|g|+3$;

 $|notcov(p,g)|=|p|+|g|+ 2$;

 $|node(s,t)|= |t|+1$;

$|member(s,t)|=|t|$.

 \item  Consider a ground instance
 $$ham(g,p) \la   path(n1,n2,g,p),  cov(p,g).$$ 
 of $1)$ and suppose that $I\models  path(n1,n2,g,p)$.   So
 $|g|+1\geq |p|$. Hence $|ham(g,p)|=3|g|+4 \geq  |p|+|g|+3=|cov(p,g)|$.
  \HB


\end{enumerate}



  \end{example}

\section{Low-Acceptability}\label{sec:low}
  In the previous two sections, we have   integrated
  the notions of acyclicity and acceptability,  by means of
 a  partition of
  the program   into
  an upper  and a lower  part.  We introduced the notion of up- and
 weak  up-acceptability, where the upper part of the program
  is proven to be acceptable
 and the lower part acyclic. In order to 
   treat also the converse case,
    i.e., the upper part  being acyclic and 
 the lower part acceptable,  we introduce now
 the notion of low-acceptability.
  We follow the   structure of
    the  previous sections: first,    a motivating 
   example is presented. Next, 
 we define the notion of low-acceptability and prove
  some results. Finally, we apply this notion to  the program
 of our example.

 
  

\subsection{An Example: Graph Specialization}\label{ex:spec1}  
 Graph structures are used in AI for many applications, such as 
 the representation of  relations, situations or problems
  (see e.g.,\ Bratko, 1986).
Two typical operations  on graphs are 
 {\em find 
 a path between two given nodes\/}, and
{\em  find a subgraph 
 with some specified properties\/}.  
  The  program   {\sc specialize\/} below  uses both these 
 operations to solve the following problem.
  Given  two
 nodes $n_1,n_2$ in a graph $g$,  find a node $n$ that does not belong
 to any    acyclic path     in $g$ from $n_1$ 
 to $n_2$.
 The   program {\sc specialize\/}  consists of the clauses: 
 \begin{program}
\> $1)$ spec(N1,N2,N,G) $\la$  \\
 \> \> \> $\neg$ unspec(N1,N2,N,G). \\
\> $2)$ unspec(N1,N2,N,G) $\la$\\
\> \> \>   path(N1,N2,G,P), \\
\> \> \>  member(N,P).\\
\end{program}

\NI  augmented with the program {\sc acypath\/} of the previous section.
   The relation $spec$  is specified   as the negation of 
    $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$.   
   For instance, {\tt spec(a,b,c,[[a,b],[b,c],[a,a],[c,b]])} holds
 (Figure 4).


\Graphb{spec.eps}{8cm}{Figure 4:   
 $spec(a,b,c,[[a,b],[b,c],[a,a],[c,b]])$ holds}

   Observe  that {\sc specialize\/}   
   is not terminating: for instance,    the query
 {\tt path1(a,[b,c],d,e)} has an infinite derivation obtained 
 by
 choosing as input clause (a variant of) the clause $p3)$
 and by selecting always its rightmost literal.
    However {\sc specialize\/} 
   is left-terminating.  In order to prove this result
 using  acceptability  (Definition \ref{acp}),   we need to find a 
  model of {\sc specialize\/} that is also a model
  of $comp(${\sc specialize\/}$)$, which is rather
 difficult. Note also that  
 the notions of weak   up- and up-acceptability
  do not help to simplify the proof. 
 However, we can split {\sc specialize\/} in two subprograms:
  $P_2$ consisting of the clause 1)  and $P_1$ consisting of
    the rest of the   program.  Note that $P_2$ extends $P_1$.  
  Therefore, in order
 to show that 
  {\sc specialize\/}  is left-terminating, it is sufficient to prove
 that $P_2\setminusp P_1$ is acyclic,  that $P_1$ is acceptable,
 and that  the corresponding level mappings are suitably related.

\subsection{Low-Acceptability}

Formally, we introduce the following notion  of low-acceptability.

\begin{definition}{\tt (Low-Acceptability)}\label{lo-acc}
  Let $|\;|$ be a level mapping for $P$. Let $R$ be a set of clauses
  s.t.\  $P=P_1\cup R$ for some $P_1$, and let $I$ be  an
 interpretation   of $R$.
   $P$ is   {\em low-acceptable w.r.t.\  $|\;|$,
      $R$ and $I$} if the following conditions hold: 
\begin{enumerate}
 \item   $P_1$   extends $R$; 

\item  $P\setminusp R$ is acyclic w.r.t.\   
     $|\; |_{|P\setminusp R}$; 

\item  $R$ is acceptable w.r.t.\  $|\; |_{|R}$ and $I$; 

\item for every ground instance $H\la L_1,\dots,L_n$ 
 of a clause of $P_1$, for every $1\leq i\leq n$,
   if $L_i$ is defined in $R$
  and is not a constraint, then  $|H|\geq |L_i|$.
 
\end{enumerate}

A program is  {\em low-acceptable} if there exist
 $|\;|$,  $R$ and $I$  s.t.\
 $P$ is low-acceptable 
 w.r.t.\   $|\;|$,  $R$ and $I$.
 \HB
\end{definition}


  The   notion of {\em low-boundedness} is defined  as
  in the previous section, by replacing  $|Q|^{up,I}_i$  
  with 
  $$|Q|^{low,I}_i =\{ |L'_i|\,\mid\, L'_1,\dots,L'_n \mbox{ is a ground instance
 of $Q$ and $I \models L'_{k_1}\wedge\dots\wedge L'_{k_{l}}$}\},$$
 where $L'_{k_1},\dots, L'_{k_{l}}$ are  the literals of 
 $ L'_1,\dots,L'_{i-1}$   whose relations occur in  $R$.
 
 To prove the analogue of Theorem \ref{mod} for low-bounded
 queries, we associate with
   a low-bounded query $Q$   a pair 
 $\pi(Q)_{low,I}=(|[Q]|_{low,I,P_1}, |[Q]|_{low,I,R})$ of 
    multisets, with 
 for  a program $P$ and an interpretation $I$  
 $$|[Q]|_{low,I,P}=bag( max |Q|^{low,I}_{k_1},\dots , 
 max |Q|^{low,I}_{k_m}),$$ 
   where $L_{k_1},\dots,L_{k_m}$ are the literals of $Q$ 
  whose relations occur in $P$. 


 

\begin{theorem}\label{modlo}
 Suppose that $P$ is low-acceptable  w.r.t.\ 
       $|\; |$, $R$ and $I$. 
 Let $Q$ be a low-bounded query. Then every
  {\tt ldcnf}-derivation for $Q$ in   $P$ contains only low-bounded
 queries and is finite. 
\end{theorem}
\Proof  
 The   proof is similar to that
  of Theorem \ref{mod}, where one replaces $\pi(Q)_{up,I}$
  with $\pi(Q)_{low,I}$.
\HB
\VV

The   following result is a direct
 consequence of Theorems \ref{modlo}  and  
 \ref{acc-5}. 
 \begin{corollary}\label{equi-l}
A  general  logic program  is low-acceptable  if and only if
 it is acceptable.
\end{corollary}


\begin{example}{\tt ({\sc specialize\/}  is Low-Acceptable)}\label{ex:spec}
  We show  that the program {\sc specialize\/}  is low-acceptable.
  Consider  the program 
  {\sc spec1}$=${\sc specialize\/}$\setminus\{ 1)\}$.
 Then the proof proceeds as follows.
     
 
\begin{enumerate}
\item  The program  $\{ 1)\}$ extends  {\sc spec1}.
\item The program  $\{ 1)\}\setminusp${\sc spec1} is 
 acyclic w.r.t.\  the level mapping

$|spec(n1,n2,n,g)|= 3|g|+5$.

\item  The program  {\sc spec1} is acceptable w.r.t.\  
   $|\; |$ and the interpretation $I$, with
    $|\; |$  
    defined  as in Example \ref{ex:weak-up} 
  for   atoms with relation $member$, $path1$,
 $path$, and  $|unspec(n1,n2,n,g)|=  3|g|+4$; and with
   $I= I_{unspec}\cup I_{path}\cup I_{path1}\cup I_{member}$,
   s.t.: 

$I_{unspec}= [unspec(N1,N2,N,G)]$,

 and  $I_{path}$, $I_{path1}$, and $I_{member}$  are  as before 
  (Example \ref{ex:weak-up}). 
\item  Consider a ground instance 

 $spec(n1,n2,n,g) \la \neg unspec(n1,n2,n,g)$

of $1)$. Then


$ |spec(n1,n2,n,g)|= 3|g|+5 \geq  3|g|+4 = |unspec(n1,n2,n,g)|$.
\end{enumerate}
 

 





 Consider  the query $Q=\mbox{{\tt spec(a,b,X,[[a,b],[b,c],[a,a]])}}$.
 Because $Q$   is low-bounded,
    it has  a finite 
 {\tt ldcnf}-tree, with answer $X \not =a , X \not =b$. 
 Notice that by using negation as failure
 $Q$   flounders.
 \HB
\end{example}
\section{A Methodology for Proving Left-Termination}\label{sec:met}
 Definitions \ref{e-acc}, \ref{def:wup}  and \ref{lo-acc} provide  a
 method for proving left-termination of a {\sc glp\/}, which is summarized
 in Definition \ref{def:method} below. In this section, we first
 discuss  advantages and drawbacks of this method. Next, we introduce 
 a methodology
 for proving left-termination of {\sc glp\/}'s that incorporates the notions
  we have introduced in the previous sections.
 Finally, we give an example in order to
  illustrate the methodology.
\begin{definition}{\tt (A Method for Proving Left-Termination)}\label{def:method}
\begin{enumerate}
\item Find a maximal set $R$ of clauses of $P$ 
 s.t.\ $R$ forms an acyclic program and $P=P_1\cup R$ is s.t.\
 either $R$  extends $P_1$ or vice versa.
\item If $R$ extends $P_1$ then:
\begin{enumerate}
 \item Prove that $P\setminusp R$ is acceptable w.r.t.\ a level mapping,
 say $|\;|_{P\setminusp R }$, and an interpretation.
\item   Use $|\;|_{P\setminusp R}$    to define a level mapping $|\;|_R$
 for $R$ s.t.\ $R$ is acyclic w.r.t.\ $|\;|_R$, and s.t.\  for every
 ground instance $H\la L_1,\dots,L_n$ of a clause of $R$,
  for every $1\leq i\leq n$:  if $L_i$ is defined in $P_1$
  then $|H|_R\geq |L_i|_{P\setminusp R } $ holds. 
\end{enumerate}
\item If $P_1$ extends $R$ then:
 \begin{enumerate}
 \item Prove that $R$ is acyclic w.r.t.\ a level mapping,
 say $|\;|_R $.
 \item   Use $|\;|_ R$ to define a level mapping $|\;|_{P\setminusp R }$
 for $P\setminusp R$ s.t.\ $P\setminusp R$ is
  acceptable w.r.t.\ $|\;|_{P\setminusp R }$
 and an interpretation $I$, and s.t.\  for every
 ground instance $H\la L_1,\dots,L_n$ of a clause of $P_1$,
  for every $1\leq i\leq n$:   if $L_i$ is defined in $R$
   and if those literals among $L_1,\dots,L_i$ 
 whose relations occur in $P\setminusp R$, say $L_{i1},\dots,L_{ik}$, are s.t.\ 
      $I\models L_{i1},\dots,L_{ik}$,  
   then  $|H|_ {P\setminusp R }\geq |L_i|_R$  holds. \HB
\end{enumerate}

\end{enumerate}
\end{definition}

  An advantage if this method is that it partly overcomes a drawback of   the original 
  method of Apt and Pedreschi to prove left-termination,
 where  one has to find a \good model of the {\em entire \/}   program. 
   Unfortunately,  our method is not always applicable.
 This happens because in     point  2. we use  $P\setminusp R$, 
 thus discarding   the literals of $R$ occurring in $P_1$. 
  These literals could be relevant for the left-termination behaviour 
 of  $P_1$. For instance,
 in the program
\begin{program}
 \> p $\la$ q,   p.\\
\> q $\la$ s.
\end{program}

  \NI  if we take $P_1$ and  $R$ to be the first and second clause,
 respectively,  then $P_1$ extends $R$, but
  $P_1\setminusp R$ is {\tt  p$\la$   p},  a  clearly  non-acceptable program.
   This problem can be overcome  by considering also  some semantic information
 about  $R$,  which leads to  the following alternative definition
 of up-acceptability.
 
  
\begin{definition}{\tt (New Up-Acceptability)}\label{new-e-acc}
 Let $|\;|$ be a level mapping for $P$. Let $R$ be  
  s.t.\ $P=P_1\cup R$ for some $P_1$,  
 let  $I_R$ be a \good model of $R$, and  let
   $I_{P_1} $ be a \good model of  $P\setminusp R$.
   $P$ is   {\em new up-acceptable w.r.t.\ $|\;|$, 
      $R$, $I_R$ and $ I_{P_1}$\/}
  if the following conditions hold:
\begin{enumerate}
 \item    $P_1$   extends $R$;
   \item   for
all ground instances $H\la L_1,\dots,L_n$ of clauses of $P_1$,
 for  every  $1 \leq i \leq \overline{n}$, with
$$\overline{n} =min (\{ n\}\cup \{j\in [1,n]\; | 
\; I_R\cup I_{P_1}\not\models
 L_j\}),$$
\begin{itemize}
  \item if $L_i$ is   defined in $P\setminusp R$  then
    $|H|>|L_i|$,
 \item if $L_i$ is   defined in $R$ then $|H|\geq |L_i|$.
\end{itemize}
  \item  $R$ is acyclic w.r.t.\    $|\; |$. \HB
\end{enumerate}
\end{definition}

 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.
\begin{example}
 Consider again  the program 

\begin{program}
 \> $1)$ p $\la$ q, p.\\
\> $2)$ q $\la$ s.
\end{program}

We prove that it is new up-acceptable.
\begin{enumerate}
\item The program  $\{1)\}$ extends $\{2)\}$;
\item Consider  the level mapping

 $|p|=1$, $|q|=1$, $|s|=0$,
 
  and the interpretations

  $I_{\{1)\}}=\{p\}$,   $I_{\{2)\}}=\emptyset$.


 Then  $I_{\{1)\}}$ and $I_{\{2)\}}$ are   \good models
 of $\{1)\}$ and of $\{2)\}$, respectively.
 We have that  $I_{\{1)}\cup I_{\{2)\} }\not\models q$
 and $|p|=|q|$.
\item From $|q|=1> 0=|s|$ it follows that $\{2)\}$ is acyclic
 w.r.t.\ $|\;|$.
\HB
\end{enumerate}
\end{example}
 
  Observe that Definition \ref{new-e-acc} 
  is still not applicable in some cases, for instance to 
 the program


\begin{program}
 \> $1)$ p $\la$ q, $\neg$ p.\\
\> $2)$ q $\la$ s.
\end{program}

\NI because the program $\{1)\}\setminusp\{2)\}$ has no \good 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  iteratively to the
  subprograms  until  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 ${\cal B}_P$ denotes the Herbrand base
  of $P$.
  
 
   
\begin{definition}{\tt (An Incremental Method)}\label{def:met2}
\begin{itemize}
 
\item Split $P$ into $n\geq 1$ parts,  say $P_1, \dots,P_n$
  s.t.\ for every $i\in [1,n-1]$:  
\begin{itemize}
 \item $P_{i+1}$  (weakly) extends $P_i$;
   \item   either $P_i$ or
 $P_{i+1}$ is acyclic.
\end{itemize}

\item Define incrementally the level mapping 
 $|\;|_{P_1\cup\dots\cup P_n}=|\;|_{P_1}\cup \dots\cup |\;|_{P_n}$
  and the interpretation
 $I_{P_1\cup\dots\cup P_n}=I_{P_1}\cup \dots\cup I_{P_n}$ as follows.
 \begin{enumerate}
\item  (base) If $P_1$ is acyclic then find the corresponding
   level mapping  $|\;|_{P_1}$;
  otherwise   prove that
  $P_1$ is acceptable w.r.t.\ a level mapping
 $|\;|_{P_1}$ and an interpretation $I_{P_1}$. 
\item  (induction) Suppose that  $|\;|_{P_k}$ is  defined
 for every $1\leq k\leq i$,
 and suppose  that $I_{P_k}$ is defined for every $1\leq k<i$ if $P_i$ is acyclic, and for every  $1\leq k\leq i$ if $P_i$ is acceptable,
 with 
    $1\leq i<n$. Then,
\begin{enumerate}
\item   If  $P_{i+1}$ is acyclic then 
 use   $|\;|_{P_i}$ 
 to define a level mapping $|\;|_{P_{i+1}}$
 for $P_{i+1}\setminusp P_i$ s.t.\ $P_{i+1}\setminusp P_i$ 
  is acyclic w.r.t.\ $|\;|_{P_{i+1}}$, 
  and  s.t.\ for all
  ground instances $H\la L_1,\dots,L_m$ of  clauses of $P_{i+1}$,
  for every $1\leq j\leq m$, if $L_j$ is defined in $P_i$ 
  then $|H|_{P_{i+1}}\geq |L_j|_{P_i}.$

\item    If  $P_{i}$ is acyclic then 
 use   $|\;|_{P_i}$ 
 to define a
  level mapping $|\;|_{P_{i+1}}$
 for $P_{i+1}\setminusp P_i$ s.t.:
\begin{enumerate}
 \item 
\begin{enumerate}
\item   either $P_{i+1}\setminusp P_i$  is acceptable
 w.r.t.\ a \good 
   model $I_{P_{i+1}}$ and $|\;|_{P_{i+1}}$; in this case set
  $I_{P_i}$ to be ${\cal B}_{P_i}$;
 \item   or find a \good model $I_{P_i}$ of 
 $P_i\setminusp P_{i-1}$, and  a \good
 model $I_{P_{i+1}}$ of $P_{i+1}\setminusp P_i$ s.t.\ for all
   ground instances  $H\la L_1,\dots,L_m$ of  clauses of $P_{i+1}$
 and  for  every  $1 \leq k  \leq \overline{m}$ if $L_k$ is 
   defined in $P_{i+1}$
  then
    $|H|_{P_{i+1}}>|L_k|_{P_{i+1}}$.
\end{enumerate}
\item   
   For all
 ground instances $H\la L_1,\dots,L_m$ of  clauses of $P_{i+1}$ and
 for  every  $1 \leq k  \leq \overline{m}$ if $L_k$ is  
  defined in  $P_i $
   then    $|H|_{P_{i+1}}\geq |L_k|_{P_i}$. 

\end{enumerate}
 Above, $\overline{m} =min (\{ m\}\cup \{j\in [1,m]\; | 
\; I_{P_{1}\cup \dots\cup P_{i+1}}\not\models
 L_j\}).$

 \HB
 \end{enumerate}
\end{enumerate}
\end{itemize}
\end{definition}




 
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.

\begin{definition}{\tt (Bounded Query)}\label{def:tb}
  Suppose that the partition $P_1,\dots,P_n$ of $P$, 
   $|\;|_{{P_1\cup\dots\cup P_n}}$ and $I_{{P_1\cup\dots\cup P_n}}$
  are obtained using the method of Definition \ref{def:met2}.
 Let $Q=L_1,\dots,L_m$.  Then $Q$ is {\em bounded (w.r.t.\ 
 $|\;|$ and $I_{{P_1\cup\dots\cup P_n}}$)}
 if  for  every $1\leq i\leq m$, the set \\
  

$|Q|^{I_{{P_1\cup\dots\cup P_n}}}_i =\{ |L'_i|\,\mid\,
 L'_1,\dots,L'_n 
 \mbox{ is a ground instance
 of $Q$ and}$

 $\qquad \qquad \qquad  I_{{P_1\cup\dots\cup P_n}} \models 
L'_{1}\wedge\dots\wedge L'_{i-1}\}$\\

 \NI  is finite. \HB
\end{definition}
 

 \begin{theorem}
 Suppose that the partition $P_1,\dots,P_n$, 
   $|\;|_{{P_1\cup\dots\cup P_n}}$ and $I_{{P_1\cup\dots\cup P_n}}$
  are obtained using the method of Definition \ref{def:met2}.
 Let $Q$ be a bounded query w.r.t.\ $|\;|_{{P_1\cup\dots\cup P_n}}$ 
 and $I_{{P_1\cup\dots\cup P_n}}$. 
 Then every {\tt ldcnf}-derivation of $Q$ is finite
 and it contains only bounded
 queries.
\end{theorem}
\Proof
  Recall that $I_{{P_1\cup\dots\cup P_n}}=
 I_{P_1}\cup \dots\cup I_{P_n}$.
  For a bounded query $Q=Q_1,\dots,Q_m$, we define the  $n$-tuple
  $\pi(Q)_{I_{{P_1\cup\dots\cup P_n}}}=(|[Q]|_{I_{P_n},P_n\setminusp P_{n-1}}, 
\dots,|[Q]|_{I_{P_2},P_2\setminusp P_{1}}, |[Q]|_{I_{P_1},P_1})$ of 
    multisets, with 
for  a program $P$,  and an interpretation  $I$,
 $|[Q]|_{I,P}=bag( max |Q|^{I}_{k_1},\dots , 
 max |Q|^{I}_{k_m}),$ 
   where $L_{k_1},\dots,L_{k_m}$ are the literals of $Q$ whose
 relations occur in  $P$. 
 The  proof is similar to the one of Theorem \ref{mod}.
\HB
\VV


  
In the following section we illustrate the application
 of this method.

\subsection{An Example: Graph Reduction}\label{ex:reduction}
   In Example \ref{ex:spec},  a program  is 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 {\sc reduce\/}
   which for  a non-empty graph $g$ and two nodes $n1$ 
 and $n2$, computes  the graph  $g'$ obtained from $g$
 by removing 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).


\Graphb{rem.eps}{12cm}{Figure 5:   
 $rem(a,b,[[a,b],[b,c],[a,a],[c,b]],[[a,b],[a,a]] )$ holds}


 The   program {\sc reduce\/}  consists of the clauses: 
 \begin{program}
\> $1)$ red(N1,N2,G1,G2) $\la$  \\
 \> \> \>  $\neg$ unif(G1,[]),\\
 \> \> \>  spec(N1,N2,N,G1),\\
  \> \> \> rem(N,G1,G),\\
  \> \> \> red(N1,N2,G,G2). \\
\> $2)$ red(N1,N2,G,G) $\la$  \\
\> \> \>  $\neg$   spec(N1,N2,N,G).\\
\> $3)$ rem(N,[[X,Y]|G1],G2) $\la$  \\
\> \> \> member(N,[X,Y]),\\
 \> \> \> rem(N,G1,G2).\\
 \> $4)$ rem(N,[[X,Y]|G1],[[X,Y]|G2]) $\la$  \\
 \> \> \> $\neg $ member(N,[X,Y]),\\
 \> \> \> member(N,G1),\\
 \> \> \> rem(N,G1,G2).\\
 \> $5)$ rem(N,[],[]) $\la$.  \\
\> $6)$ unif(G,G) $\la$. 
\end{program}

\NI  plus  the program {\sc specialize\/}. The relation $red(n1,n2,g,g')$
 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  
 belong to 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   {\sc reduce\/}   is 
   left-terminating by using our  bottom-up method. 
  {\sc reduce\/} can be partitioned in three parts:
\begin{itemize}
 \item $P_1$  is
   the program {\sc spec1} of Example \ref{ex:spec};
 \item $P_2$ consists of the clauses 3), 4), 5)  of {\sc reduce\/}
  plus the clauses 1), p4), p5)   of {\sc specialize\/};
 \item  $P_3$  consists of the
    clauses 1), 2), and 6) of {\sc reduce\/}. 
\end{itemize}
  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.\ $\{member\}$.
 So  we can apply the bottom-up approach to construct a level
 mapping $|\;|_{P_1\cup P_2\cup P_3}$ and an interpretation 
 $I_{P_1\cup P_2\cup P_3}$. The proof proceeds as follows.
\begin{itemize}
\item   $P_1$ is acceptable w.r.t.\ $|\;|_{P_1}$ and  $I_{P_1}$
   given in Example  \ref{ex:spec}.  
\item $P_2\setminusp P_1$ is acyclic w.r.t.\ $|\;|_{P_2}$ defined as in
 Example  \ref{ex:spec} for $spec$ and $member$, and s.t.\ 
 
 $|rem(n,g1,g2)|_{P_2}=|g1|+2$.

 Moreover, clause 1) of {\sc specialize\/} satisfies
  the  condition relating
   the two level mappings.
\item In order to define  $|\;|_{P_3}$, $I_{P_3}$ and $I_{P_2}$,
  we apply point i.B. 
  Consider the level mapping
  



  $|red(n1,n2,g1,g2)|_{P_3}=3|g1|+5$,

 $|unif(g,g)|_{P_3}=0$,


 and let

 $I_{P_2}=\{ rem(n,g1,g2) \, \mid \, \mbox{$g1$,
 $g2$ lists and 
  either $g1=g2=[\;]$ or  $|g2| < |g1|$}\}
\cup$ 

$\qquad \cup [spec(X,Y,Z,W)]\cup\{member(n,g)\, \mid \, \mbox{$g$ list and
 $n$ in $set(g)$}\},$ 
 
   $I_{P_3}=[red(N1,N2,G1,G2)]\cup \{ unif(x,y) \, \mid \, x=y\}.$ 
 
 It is easy to check that $I_{P_2}$ and
  $I_{P_3}$ are \good models of $P_2\setminusp P_1$ and $P_3\setminusp P_2$,
 respectively. It remains to check the tests in points i.B and ii.
\begin{itemize}
\item Consider a ground instance 

 $$\begin{array}{ll}
 red(n1,n2,g1,g2)\la & \neg unif(g1,[\;]), spec(n1,n2,n,g1),\\
   & rem(n,g1,g),
 red(n1,n2,g,g2).
\end{array}$$

\NI of 1). We have that:\medskip

 $|red(n1,n2,g1,g2)|_{P_3}=3|g1|+5 > 0= |\neg unif(g1,[\;])|_{P_3}$;
\smallskip

 $|red(n1,n2,g1,g2)|_{P_3}=3|g1|+5 = |spec(n1,n2,n,g1)|_{P_2}$;\smallskip

 $|red(n1,n2,g1,g2)|_{P_3}=3|g1|+5 > |g_1|+2=|rem(n,g1,g)|_{P_2}$.\medskip



  Now, suppose that $I_{P_2}\cup I_{P_3}\models \neg unif(g1,[\;]), 
 rem(n,g1,g)$.
 Then $g$ and $g1$ are lists, 
   $g1\neq [\;]$, and  $|g|< |g1|$. Then,\medskip

 $|red(n1,n2,g1,g2)|_{P_3}=3|g1|+5 > 3|g|+5=| red(n1,n2,g,g2)|_{P_3}$.
\medskip
 
\item Consider a ground instance 
$$ red(n1,n2,g,g)\la \neg spec(n1,n2,n,g).$$
\NI of 2). We have that:

 $|red(n1,n2,g,g)|_{P_3}=3|g|+5 = |spec(n1,n2,n,g)|_{P_2}$.
\end{itemize}


\end{itemize}
Observe that the presence of the literal $\neg 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)$).
 
 

  
\section{Conclusion}\label{sec:con}
In this paper we proposed  simple methods  for
 proving  termination of a general logic program,
 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 minimalized. 
  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)  introduced a modular approach for
 proving acceptability of logic programs, i.e.,
  they do not deal with   programs
 containing negated atoms.  Proving
 termination of {\em general\/} logic  programs in a modular
 way, using the notion of acceptability, seems a  rather difficult task,
  because it amounts  to
  building a model of the completion of a program by  combining 
    models of the completions  of 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 \ref{sec:met}.
  
   
   
  
\section*{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 proposing
   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. 
 
 
\vskip 0.2in
\bibliography{jair-fin}
\bibliographystyle{theapa}




\end{document}








