
% Submitted to J. of Logic Prog.

\documentstyle[jlp,twoside]{article}

\newcommand{\var}{\varphi}
\newcommand{\D}{\:\: |\:\:}
\newcommand{\ttl}{\subsubsection*}
\newcommand{\rto}{\rightarrow}
\newcommand{\lto}{\leftarrow}
\newenvironment{lprule}{\begin{center}\tt\begin{tabular}{l}}{\end{tabular}\end{center}}
\newenvironment{myenu}{\begin{enumerate}\setlength{\itemsep}{0.0pt}}{\end{enumerate}}
\newenvironment{myitem}{\begin{itemize}\setlength{\itemsep}{0.0pt}}{\end{itemize}}
\long\def\comment#1{}
\newcommand{\align}{&\hspace{-.2in}&}
\newcommand{\aligna}{\hspace{.1in}&}
\newcommand{\tab}{\hspace*{.2in}}
%\newcommand{\mand}{\!\circ\!}
\newcommand{\mand}{\mbox{\scriptsize $\;\&\;$}}
\newcommand{\cut}{\mbox{\tt !}}
\newcommand{\new}[1]{\widehat{#1}}

\begin{document}

\main{Rules as Actions:
A Situation Calculus Semantics for Logic Programs}{
Fangzhen Lin and Ray Reiter\thanksone{Fellow of the Canadian Institute
for Advanced Research}\affil{
Department of Computer Science,
University of Toronto,
Toronto, Canada M5S 1A4.
Email: \{fl,reiter\}@ai.toronto.edu. 
http://www.cs.toronto.edu/\~\ \hspace{-.4em}cogrobo/}}

\bibliographystyle{abbrv}

\begin{abstract}
We propose a novel semantics for logic programs with negation
by viewing the application of a clause in a derivation as an action 
in the situation calculus. Program clauses 
are then identified with situation calculus effect axioms as they are understood
in axiomatic theories of actions. We then solve the frame problem for these
effect axioms using a recent approach of Reiter \cite{Reiter91}, and 
identify the
resulting collection of axioms with the semantics of the original logic 
program.
An interesting consequence of this approach is
that the logic programming negation-as-failure operator
inherits its
nonmonotonicity from the nonmonotonicity associated with the frame problem.

One advantage
of our proposal is that like Clark's completion semantics, ours is
also formulated explicitly in classical logic. To illustrate
the usefulness of
our semantics, we prove sufficient conditions for two
logic programs to be equivalent, and use this to verify the
correctness of the well-known unfolding
program transformation operator.
We also discuss applications
of this framework to formalizing search control operators
in logic programming.
\end{abstract}

\noindent {\bf Keywords}. Semantics of logic programs. Reasoning about actions.
The situation calculus. The frame problem.


\section{Introduction}

In this paper we propose a novel semantics for
logic programs
in the situation calculus. One of the advantages of our proposal is that
like Clark's completion semantics, it is explicitly formulated in classical
logic. For this reason,
it is suitable for proving properties of logic programs such
as the correctness of various program transformation operators.

The basic idea of our proposal is very simple. We consider
the application of a clause in a derivation to be an action
in the situation calculus (McCarthy \cite{mccarthy63}). 
Executing a clause makes the head of the
clause true in the new situation whenever the body of the clause is true in
the current situation. Program clauses
are then identified with situation calculus effect axioms as they are understood
in axiomatic theories of actions. We then solve the frame problem for these
effect axioms using a recent approach of Reiter \cite{Reiter91}, and
identify the
resulting collection of axioms with the semantics of the original logic
program.

This paper is organized as follows. In the next section, we
briefly review the situation calculus and the frame problem.
Section 3 provides the necessary logical
preliminaries, and Section 4 defines our situation calculus semantics for
logic programs. Section 5 shows some relationships between our
semantics and Wallace's \cite{Wallace93}, and also relates our
semantics to the stable model semantics \cite{GelfondLifschitz88}.
Section 6 formulates
conditions for two logic programs to be equivalent and
applies this result to verifying the correctness of the unfolding program
transformation operator. Section 7 discusses other potential
applications of our semantics, while
Section 8 provides some concluding remarks.

\section{An Informal Introduction to the 
Situation Calculus\protect\footnotemark}
\addtocounter{footnote}{0}\footnotetext{This
section is included in order to make this paper as self contained as
possible. With minor differences, it is the same as that of Levesque et al 
\cite{levesquereiter:golog}.}

\subsection{Intuitive Ontology for the Situation Calculus}
The situation calculus (McCarthy \cite{mccarthy63}) is a first order
language (with, as we shall see later, some second order features)
specifically designed for representing dynamically changing worlds. All
changes to the world are the result of named {\it actions}.
A possible world history, which is simply a sequence of actions,
is represented by a first order term called
a {\em situation}.
The constant $S_0$ is used to denote the {\em initial situation}, namely that
situation in which no actions have yet occurred.
There is a distinguished binary function symbol $do$; $do(\alpha,s)$ denotes
the successor situation to $s$
resulting from performing the action $\alpha$.
Actions may be parameterized. For example, $put(x,y)$ might stand for the
action
of putting object $x$ on object $y$, in which case $do(put(A,B),s)$
denotes the situation resulting from placing $A$ on $B$ when the world is in
situation $s$.
Notice that in the situation calculus, actions are denoted by first order
terms,
and situations (world histories) are also first order terms. For example,
$do(putdown(A),do(walk(L),do(pickup(A),S_0)))$ is a situation denoting the
world history consisting of the sequence of actions
[pickup(A), walk(L), putdown(A)]. Notice that the sequence of actions in a
history, in the
order in which they occur, is obtained from a situation term by reading off the
actions from right to left.

Generally, the values of relations in a dynamic world  will
vary from one situation to the next.
Such relations are called
{\em fluents}, and are
denoted by predicate symbols taking a situation term as
one of their arguments. The convention we shall adopt is that the situation
argument
of a fluent will always be its last argument. For example,
in a mobile robot environment, we might have a relational fluent
$closeTo(r,x,s)$ meaning that in situation $s$
the robot $r$ is close to the object $x$.

\subsection{Axiomatizing Actions and their Effects in the Situation Calculus}

Actions have {\it preconditions} -- necessary and sufficient conditions that
characterize when the action is physically possible. For example, in a
blocks world, we might have:\footnote{
In formulas, free variables are considered to be 
universally quantified from the
outside. This convention will be followed throughout the paper.}
$$
\begin{array}{l}
Poss(pickup(x),s) \equiv \\ \hspace{2em}
[(\forall z)\neg holding(z,s)] \wedge nexto(x,s)\wedge \neg heavy(x).
\end{array}
$$

World dynamics are specified by {\it effect axioms}.
These describe the effects of a given action on the
fluents -- the causal laws of the domain. For example, a robot
dropping a fragile
object causes it to be broken:
\begin{equation}
\label{broken1}
Poss(drop(r,x),s) \wedge fragile(x,s)
\supset broken(x,do(drop(r,x),s)).
\end{equation}
Exploding a bomb next to an object causes it to be broken:
\begin{equation}
\label{broken2}
Poss(explode(b),s) \wedge nexto(b,x,s) \supset
broken(x, do(explode(b),s)).
\end{equation}
A robot repairing an object causes it to be not broken:
\begin{equation}
\label{broken3}
Poss(repair(r,x),s) \supset \neg broken(x,do(repair(r,x),s)).
\end{equation}

\subsection{The Frame Problem}
As first observed by McCarthy and Hayes \cite{McCarthyHayes69}, 
axiomatizing a dynamic world
requires more than just action precondition and effect axioms. So-called
{\em frame axioms} are also necessary. These specify the action {\it invariants}
of the domain, namely, those fluents which remain unaffected by a given action.
For example, a robot dropping things does not affect an object's color:
$$
Poss(drop(r,x),s) \wedge color(y,c,s)
\supset color(y,c,do(drop(r,x),s)).
$$
A frame axiom describing how the fluent $broken$ remains unaffected:
$$
\begin{array}{l}
Poss(drop(r,x),s) \wedge \neg broken(y,s) 
\wedge [y \neq x \vee \neg fragile(y,s)
]\\
\hspace{5em}\supset \neg broken(y,do(drop(r,x),s)).
\end{array}
$$

The problem introduced by the need for such frame axioms is that we can
expect a vast number of them. Only relatively
few actions will
affect the truth value of a given fluent;
all other actions leave the fluent
invariant. For example,
an object's color is not changed by
picking things up, opening a door, going for a walk,
electing a new prime minister of Canada, etc.
This is problematic for the axiomatizer -- she must think of all these axioms --
and it is problematic for the theorem proving system -- it must reason
efficiently in the presence of so many frame axioms.

\subsubsection{What Counts as a Solution to the Frame Problem?}
Suppose the person responsible for axiomatizing an application
domain has specified all of the causal laws for the world being axiomatized.
More precisely, she has succeeded in writing down {\em all}
the effect axioms, i.e.
for each
fluent $F$ and each action A which can cause $F$'s truth value to
change,
axioms of the form
$$
Poss(A,s) \wedge R({\vec x},s) \supset (\neg)F({\vec x},do(A,s)).
$$
Here, $R$ is a first order formula specifying the contextual conditions
under which the action $A$ will have its specified effect on $F$.

A solution to the frame problem
is a systematic procedure for generating, from these effect axioms,
all the frame axioms.
If possible, we also want a {\em parsimonious} representation for these
frame axioms (because in their simplest form, there are too many of them).

\subsection{A Simple Solution to the Frame Problem}
By appealing to earlier ideas of Haas \cite{Haas87}, Schubert \cite{Schubert90} and
Pednault \cite{pednault89}, Reiter \cite{Reiter91} 
proposes a simple solution to the frame
problem, which we illustrate with an example.
Suppose that (\ref{broken1}), (\ref{broken2}), and (\ref{broken3}) 
are all the effect axioms
for the fluent $broken$, i.e. they describe all the ways that an action
can change the truth value of $broken$. We can rewrite (\ref{broken1}) and 
(\ref{broken2})
in the logically equivalent form:
\begin{equation}
\begin{array}{l}
Poss(a,s) \wedge [(\exists r)\{a = drop(r,x) \wedge
fragile(x,s)\}\\
\hspace{3em} \vee (\exists b)
\{a = explode(b) \wedge nexto(b,x,s)\}]\\
\hspace{6em} \supset broken(x,do(a,s)).
\label{broken}
\end{array}
\end{equation}
Similarly, consider the negative effect axiom (\ref{broken3}) for {\it broken};
this can be rewritten as:
\begin{equation}
Poss(a,s) \wedge (\exists r)a = repair(r,x) \supset
\neg broken(x,do(a,s)).
\label{unbroken}
\end{equation}

In general, we can assume that the effect axioms for a fluent $F$ have been 
written in the forms:
\begin{equation}\label{poseffect}
\mbox{\em Poss}(a,s)\,\wedge \,\gamma_{F}^{+}(\vec{x},a,s) \;\supset\;
F(\vec{x},do(a,s)),
\end{equation}
\begin{equation}\label{negeffect}
\mbox{\em Poss}(a,s)\,\wedge \,\gamma_{F}^{-}(\vec{x},a,s) \;\supset\;
\neg F(\vec{x},do(a,s)).
\end{equation}
Here $\gamma_{F}^{+}(\vec{x},a,s)$ is a formula describing under what
conditions doing the action $a$ in situation $s$ leads the fluent $F$
to become true in the successor situation $do(a,s)$; similarly
$\gamma_{F}^{-}(\vec{x},a,s)$ describes the conditions under
which performing $a$ in $s$ results in $F$
becoming false in the next situation.
The solution to the frame problem of
\cite{Reiter91}
rests on a {\em completeness assumption\/}, which is
that the causal axioms~(\ref{poseffect}) and~(\ref{negeffect})
characterize
all the conditions under which action $a$ can lead to a fluent $F(\vec{x})$
becoming true (respectively, false) in the successor situation.
In other words, axioms~(\ref{poseffect}) and~(\ref{negeffect}) describe
all the
causal laws affecting the truth values of the fluent $F$.
Therefore, if action $a$ is possible and $F(\vec{x})$'s truth value changes
from {\em false\/} to {\em true\/} as a result of doing $a$, then
$\gamma^{+}_{F}(\vec{x},a,s)$ must be {\em true\/} and similarly for a
change from {\em true\/} to {\em false\/}.
Reiter \cite{Reiter91} shows how to derive
a {\em successor state
axiom\/}
of the following form from
the causal axioms (\ref{poseffect}) and (\ref{negeffect}) and
the completeness assumption.\\[.7ex]
\noindent {\bf Successor State Axiom\/}
$$
Poss\,(a,s)\,\supset \, [ F(\vec{x},do(a,s))\,\equiv
\gamma_{F}^{+}(\vec{x},a,s)\,\vee\, (F(\vec{x},s)\, \wedge\, \neg
\gamma_{F}^{-}(\vec{x},a,s))]
$$
This single axiom embodies a solution to the frame problem.
Notice that this axiom universally quantifies over actions $a$. In fact, this
is one way in which a parsimonious solution to the frame problem is
obtained.

Applying this to our example about breaking things, we obtain the following 
successor state axiom:
$$
\begin{array}{l}
Poss(a,s) \supset [broken(x,do(a,s)) \equiv \\
\hspace{4em} (\exists r)\{a = drop(r,x) \wedge fragile(x,s)\} \;\vee\\
\hspace{4em} (\exists b)\{a = explode(b) \wedge nexto(b,x,s)\} \;\vee\\
\hspace{4em} broken(x,s) \wedge \neg (\exists r)a = repair(r,x)].
\end{array}
$$

It is important to note that the above solution to the frame problem 
presupposes that there are no {\em state constraints}, as for example in the
blocks world constraint: $(\forall s).on(x,y,s) \supset \neg on(y,x,s)$.
Such constraints sometimes implicitly contain effect axioms (so-called
indirect effects), in which case the above completeness assumption will not
be true.

In what follows, we shall provide a semantics for logic programs, with negation,
by treating the application of a rule (clause) in a derivation as an action
in the situation calculus. Program clauses will then be identified with
effect axioms. By solving the frame problem exactly as just described,
we shall obtain a situation calculus representation of
the program which will serve as the program's logical semantics. 

As is well known, solutions to the frame problem are nonmonotonic, in the
sense that the above completeness
assumption (the given effect axioms are all and only
the effect axioms) is a kind of closed world assumption. The addition of a
new effect axiom to an earlier axiomatization for some domain may 
invalidate any solution to the frame problem obtained with the earlier
axioms. This intuition has led to a large body of research on nonmonotonic
solutions to the frame problem 
(e.g. \cite{McCarthy86,Shoham88,Lifschitz:pointwise,Lifschitz:action,LinShoham95}).
In view of our situation calculus semantics for logic programming,
it will follow that 
{\em negation-as-failure 
inherits its
nonmonotonicity from the nonmonotonicity associated with the frame problem.}

\section{Logical Preliminaries}

\subsection{The Language of the Situation Calculus}

The language $\cal L$ of the situation calculus is many-sorted, second-order,
with equality. We assume the following 
sorts: {\it situation} for situations, {\it action} for actions, and {\it object}
for everything else. We also assume the following domain independent predicates
and functions: 
\begin{itemize}
\setlength{\itemsep}{0pt}
\item A constant $S_0$ of sort {\em situation} denoting the initial situation.
\item A binary function $do$ - $do(a,s)$
denotes the situation resulting from performing action $a$ in situation $s$.
\item A binary predicate $Poss$ - $Poss(a,s)$ means that
action $a$ is possible (executable) in situation $s$.
In this paper we shall assume that actions are always executable, i.e.
$(\forall a,s)Poss(a,s)$. So technically, there is no real need for this
predicate in this paper. We keep it, however, in order to be consistent
with the general framework of
(Reiter \cite{Reiter91}
and Lin and Reiter \cite{LinReiter:constraint}).


\item A binary predicate $<$ over situations. We shall follow convention, 
and write $<$ in
infix form. By $s<s'$ we mean that $s'$ can be obtained from $s$ by a
sequence of executable actions. As usual, $s\leq s'$ will be a shorthand
for $s<s'\lor s=s'$. 
\end{itemize}
We assume a finite number of
{\em fluents}, which are predicate symbols of arity $object^n\times situation$,
$n\geq 0$, and are domain dependent. 
We also assume a finite number
of function symbols
of arity $object^n\rightarrow action$, $n\geq 0$, for actions,
and a finite
number of function symbols of arity $object^n\rightarrow object$,
$n\geq 0$. %These are all domain dependent as well.


\subsection{Axiomatizing the Situation Calculus}
\label{sitcalc}

We shall need the following
foundational axioms (Lin and Reiter \cite{LinReiter:constraint}) for the
situation calculus:
%\footnote{These axioms have their origin in (Reiter \cite{Reiter:<}).
%Similar axioms are used in (Pinto and Reiter \cite{PintoReiter93}).}
\begin{eqnarray*}
&  S_0\not= do(a,s),& \label{eq:foundation1}\\[1ex]
& do(a_1,s_1)=do(a_2,s_2)\supset
 (a_1=a_2\land s_1=s_2),& \label{eq:foundation2}\\[1ex]
& (\forall P)[P(S_0)\land (\forall a,s)(P(s)\supset P(do(a,s)))
 \supset (\forall s)P(s)],& \label{eq:foundation3}\\[1ex]
&  \neg s< S_0,& \label{eq:foundation4}\\[1ex]\nopagebreak[3]
& s< do(a,s')\equiv (Poss(a,s')\land s \leq s').& \label{eq:foundation5}
\end{eqnarray*}

Intuitively, the first two axioms are unique names assumptions. They eliminate 
cycles, and merging. The third axiom is second order induction. It amounts to
the domain closure axiom that
every situation is obtained from the initial one by repeatedly
applying the function $do$.\footnote{For a detailed 
discussion of the use of induction in the
situation calculus, see (Reiter \cite{Reiter:<}).} As we shall see,
induction will play an important role in this paper.
The last two axioms define $<$ inductively.

Notice the similarity between these axioms and the Peano foundational
axioms for number theory. However, unlike Peano arithmetic which has a unique
successor function, we have a class of successor functions here represented
by the function $do$.
In the following, we shall denote by $\Sigma$ the set of the above axioms.

\subsection{Logic Programs}

An {\em atom} $p$ is an expression of the form $F(t_1,...,t_n)$, where
$F$ is a fluent of arity $object^n\times situation$, and $t_1,\ldots,t_n$
are terms of sort $object$.
Notice that an atom is not a formula in the situation calculus. It
is an expression obtained from an atomic situation calculus
 formula by suppressing its
situation argument.

A {\em literal} is either an atom, or an expression of the form {\tt not~$p$},
where $p$ is an atom. 
In addition, 
an equality formula of the form $t=t'$ is a {\em literal},
where $t$ and $t'$ are terms of
sort $object$.
Again, notice that, except for equality literals,
literals are not formulas in the language
of the situation calculus. 

A {\em goal } $G$ is an expression
of the form
\begin{lprule}
 $l_1$ \& $\cdots$ \& $l_n$
\end{lprule}
where $n\geq 0$, and $l_1,\ldots,l_n$ are literals.
A {\em clause} is an expression of the form
\begin{lprule}
$F(\vec{x})$ :- $G$
\end{lprule}
where $F$ is a fluent symbol,
%$F$ is an $(n+1)$-ary fluent, 
$\vec{x}$ is a tuple of distinct variables
of length $n$, $n\geq 0$, and $G$ is a goal.
Notice that according to this definition, the head of a clause must
not mention constants and compound terms.
This, however, does not restrict the generality of our notion of clauses.
For any terms $t_1,...,t_n$ of sort $object$, we 
can take an expression of the form
\begin{lprule}
$F(t_1,...,t_n)$ :- $G$
\end{lprule}
to be a {\em shorthand} for
the following clause:
\begin{lprule}
$F(\vec{x})$ :- $\vec{x}=\vec{t}$ \& $G$
\end{lprule}
where $\vec{x}=(x_1,...,x_n)$ is a tuple of fresh variables not mentioned
in $G$
or in $\vec{t}$. 
Generally, for any vectors $\vec{t}=(t_1,...,t_k)$ and 
$\vec{t'}=(t_1',...,t_k')$ of terms of the same
length, if $\vec{t}=\vec{t'}$ appears in a goal, then it stands for
\[
t_1=t_1'\mand \cdots\mand t_k=t_k',\]
and if $\vec{t}=\vec{t'}$ appears in a situation calculus
formula, then it stands for
\[
t_1=t_1' \land\cdots\land t_k=t_k'.
\]

Finally, a {\em normal program } is a finite set of
clauses.
In the following, normal programs will simply be called programs.
The {\em definition} of a fluent symbol $F$ in a program $P$ is the
set of clauses in $P$ that mention $F$ in their head.

Since we will be interpreting clauses as formulas of the situation calculus,
we need a way to interpret literals in the situation calculus.
Given a literal $l$, and a situation term $st$, we define $l[st]$ as
follows:
\begin{enumerate}
\setlength{\itemsep}{0pt}
\item If $l$ is an atom of the form $F(t_1,...,t_n)$, 
then $l[st]$ is $F(t_1,...,t_n,st)$, i.e. it is 
the formula obtained from $l$ by putting $st$ back as its last argument.
\item If $l$ is a negated atom of the form {\tt not~$F(t_1,...,t_n)$}, then
$l[st]$ is the formula $\neg (\exists s)F(t_1,...,t_n,s)$. Notice that
in this case, the truth value of the formula $l[st]$ is independent of 
the situation $st$. {\em This is our interpretation of the 
negation-as-failure operator
``{\tt not}'' in the situation calculus.}
\item If $l$ is an equality formula of the form $t=t'$, then
$l[st]$ is $l$.
\end{enumerate}
Now if $G$ is a goal of the form $l_1 \& \cdots \& l_n$, and $st$ a
situation term, then we define $G[st]$ to be the formula
\[ l_1[st]\land\cdots\land l_n[st].\]

\subsection{Clark's Completion}

Since we shall often refer to Clark's completion \cite{Clark78}
in this paper, we briefly review it here.

A clause of the form
\begin{lprule}
$F(\vec{x})$ :- $l_1$ \& $\cdots$ \& $l_n$
\end{lprule}
stands for the following implication about $F$:
\begin{equation}
\label{clark}
(\exists \vec{y})(l_1'\land\cdots\land l_n')\supset F(\vec{x}),
\end{equation}
where $\vec{y}$ is the tuple of variables that appear in some $l_i$,
$1\leq i\leq n$, but are distinct from variables in $\vec{x}$, and if $l$ is
an atom then $l'$ is $l$, and if $l$ is $\mbox{\tt not}\ p$, 
then $l'$ is $\neg p$.

Given a logic program $P$, if
\begin{lprule}
$F(\vec{x})$ :- $G_1$\\
\tab \vdots\\
$F(\vec{x})$ :- $G_m$
\end{lprule}
is the definition of $F$, then the Clark completion of $F$ in $P$
is the following sentence:
\[
F(\vec{x}) \equiv [(\exists \vec{y_1})G_1'\land\cdots\land
(\exists \vec{y_m})G_m'],
\]
where $(\exists \vec{y_i})G_i'$, $1\leq i\leq m$,
is as the left hand side of the implication (\ref{clark}).
Notice that if $m=0$, i.e. there are no clauses in $P$ about $F$, then
the Clark completion of $F$ is $F(\vec{x})\equiv false$.

The Clark completion of a program $P$ is then the set consisting of
the following axioms: 
\begin{enumerate}
\item For
each predicate $F$ in $P$, the Clark completion of $F$ in $P$. 
\item Unique names axioms for the function symbols appearing in $P$.
\end{enumerate}

Clark's completion is perhaps the simplest semantics for logic programs.
It replaces rules in a logic program by logical axioms in first-order
logic.
The main problem with it is that it is too weak for logic programs with
cycles and recursion (see, for example, \cite{Lloyd87}).

Our proposed semantics will be very much in the same style as Clark's
completion, but it will also handle cycles and recursion correctly.

\section{A Situation Calculus Semantics for Logic Programs}
\label{semantics}

On our intuition about logic programs, clauses are treated as rules, so that
the application of such a rule in the process of obtaining a derivation is
like performing an action. So
a clause of the form
\begin{lprule}
 $F(\vec{x})$ :- $G$
\end{lprule}
is like the specification of the effects of
an action; if $G$ holds currently, then $F(\vec{x})$ will hold after the
action is performed.
Taking this intuition seriously,
suppose that we name this clause by the action 
$A(\vec{x})$ in our situation calculus
language. Then
we have the following axiom (an {\em effect axiom}) describing the effect
of $A$:
\[
Poss(A(\vec{x}),s)\supset ( G[s]\supset F(\vec{x}, do(A(\vec{x}),s)).\]
Recall from section~3.1 that we have assumed that actions
are always possible:
\[ Poss(a,s)\equiv true.\]
Thus the above effect axiom is equivalent to
\[
G[s]\supset F(\vec{x}, do(A(\vec{x}),s)).
\]
Let $\vec{y}$ be the tuple of variables in $G$ which are not
in $\vec{x}$,
then we can rewrite the above axiom as
\begin{equation}
\label{eq:effect}
(\exists \vec{y})G[s]\land a=A(\vec{x})
 \supset F(\vec{x},do(a,s)).
\end{equation}
%where $\vec{x}=\vec{t}$ is a shorthand for $x_1=t_1\land\cdots\land x_m=t_m$.
%In the following we shall call (\ref{eq:effect}) a {\em corresponding effect
%axiom} of the definite clause (\ref{eq:clause1}).
Notice the similarity, but not the formal identity, between
this transformation and that leading up to the formation of
the Clark completion of a predicate.

\begin{example}
Suppose that $gf(x,y)$ is the action naming
the following clause:
\begin{lprule}
grandfather(x,y) :- parent(x,z) \& parent(z,y) \& not female(x)
\end{lprule}
Then we have the following effect axiom:
\begin{eqnarray*}
\align (\exists z)[parent(x,z,s)\land parent(z,y,s)]\land 
\neg (\exists s')female(x,s') \land
 a=gf(x,y)
 \supset\\
\align\hspace{2em} grandfather(x,y,do(a,s)).
\end{eqnarray*}
\end{example}

Now suppose that $P$ is a program and $F$ a fluent. Suppose
the following are the corresponding effect axioms of the form (\ref{eq:effect})
for the clauses in
the definition of $F$ in $P$:
\begin{eqnarray*}
\align (\exists \vec{y_1})G_1[s]\land a=A_1(\vec{x})\supset
 F(\vec{x},do(a,s)),\\
\align\hspace{2em} \vdots\\
\align (\exists \vec{y_n})G_n[s]\land a=A_n(\vec{x})\supset
 F(\vec{x},do(a,s)).
\end{eqnarray*}
%Since the clauses in the definition of $F$ are the only rules that can
%be used to establish instances of $F$, these effects axioms include
%all the actions that may have effects on $F$. In particular, no action will
%cause $F$ to become false.
Then, by solving the frame problem for fluent $F$ as described in Section 2.4,
we obtain the
following {\em successor state axiom} for
$F$:
\begin{eqnarray}
\align F(\vec{x},do(a,s))\equiv \{(\exists \vec{y_1}) G_1[s]\land 
a=A_1(\vec{x}) \lor\cdots\lor \nonumber\\
\align\hspace{3em} (\exists \vec{y_n}) G_n[s]
 \land a=A_n(\vec{x})\lor \label{eq:succ}\\
\align\hspace{3em} F(\vec{x},s)\}. \nonumber
\end{eqnarray}
Intuitively, the successor state axiom for $F$ says that the fluent
is true in a successor situation iff either it is true in the current
situation, or the action names
one of the clauses in the definition of $F$ and the body of that clause
is true in the current situation. 
In particular, if the definition of $F$ in
the program $P$ is empty, then (\ref{eq:succ}) becomes
\[ F(\vec{x},do(a,s))\equiv F(\vec{x},s).\]

In the following, we call (\ref{eq:succ}) the {\em successor state axiom for $F$ with respect to $P$}.
Notice the similarity between this axiom
and the Clark completion of $F$.

We can now define the ``meaning'' of logic programs in the situation
calculus. We assume that for each clause there is a unique 
action symbol that names the clause, and has the same number of arguments as
that of the predicate in the head of the clause.

\begin{definition}
Let $P$ be a program. 
The {\em action theory $\cal D$ for} $P$ is
\[
{\cal D} = \Sigma\cup {\cal D}_{ss}\cup {\cal D}_{una}
\cup {\cal D}_{S_0}
\]
where
\begin{itemize}
\setlength{\itemsep}{0pt}
\item $\Sigma$ is the set of foundational axioms given in 
Section~\ref{sitcalc}.
\item ${\cal D}_{ss}$ is the set of successor state axioms for
the fluents with respect to $P$.
\item ${\cal D}_{una}$ is the set consisting of the following {\em unique names
axioms}:
\begin{equation}
f(\vec{x})\neq g(\vec{y}) \label{eq:una1}
\end{equation}
for every pair $f,g$ of distinct function
symbols, and
\begin{equation}
f(\vec{x})=f(\vec{y})\supset \vec{x}=\vec{y} \label{eq:una2}
\end{equation}
for every function symbol $f$.
Notice that constants are considered to be 0-ary functions.
We remark that for the function $do$, (\ref{eq:una2})
is the same as one of our foundational axioms in $\Sigma$.
We also remark that ${\cal D}_{una}$ includes unique names axioms for
the actions introduced to name the program clauses.
\item ${\cal D}_{S_0}$ is:
\[ \{ F(\vec{x},S_0)\equiv false\D F \mbox{ is a fluent}\}.\]
In other words, in the initial situation, all fluents are false.
\end{itemize}
\end{definition}

Notice that only the set ${\cal D}_{ss}$ of successor state axioms
is dependent on the clauses in $P$. All other sets in the above definition
either are domain independent or depend only on the vocabulary of $P$.

\begin{proposition}
Suppose, as in (\ref{eq:succ}),
that fluent $F$'s successor state axiom has the
form
$$
F(\vec{x},do(a,s)) \equiv \phi(\vec{x},a,s) \lor F(\vec{x},s),
$$
where $\phi(\vec{x},a,s)$ is any first order formula whose free variables are
among $\vec{x},a,s$.
Suppose further that $F(\vec{x},S_0) \equiv false.$
Then the foundational and unique names
axioms for the situation calculus, together
with these two sentences entail:
$$
F(\vec{x},s) \equiv (\exists a',s')[do(a',s') \leq s \land \phi(\vec{x},a',s')].
$$
\end{proposition}
\begin{proof}
The proof is by induction. The case $s = S_0$ is immediate. So, assume the
result for situation $s$. We must prove
$$
F(\vec{x},do(a,s)) \equiv (\exists a',s')[do(a',s') \leq do(a,s)
\land \phi(\vec{x},a',s')].
$$
$\Longrightarrow$\\
Assume $F(\vec{x},do(a,s))$. We must prove
\begin{equation}
\label{mustprove}
(\exists a',s')[do(a',s') \leq do(a,s)
\land \phi(\vec{x},a',s')].
\end{equation}
By $F$'s successor state axiom, we have
$\phi(\vec{x},a,s) \lor F(\vec{x},s)$.\\
{\em Case 1:} $\phi(\vec{x},a,s)$. Then take $a' = a$ and $s' = s$ in
(\ref{mustprove}) and we are done.\\
{\em Case 2:} $F(\vec{x},s)$. By induction hypothesis, we know that for some
$\alpha$ and $\sigma$, $do(\alpha,\sigma) \leq s$ and
$\phi(\vec{x},\alpha,\sigma)$.
So take $a' = \alpha$ and $s' = \sigma$ in
(\ref{mustprove}), leaving us to prove $do(\alpha,\sigma) \leq do(a,s)$; this
follows immediately from $do(\alpha,\sigma) \leq s$ and the foundational axioms
for the situation calculus.\\[.6ex]
$\Longleftarrow$\\
Assume, for some $\alpha$ and $\sigma$ that $do(\alpha,\sigma) \leq
do(a,s)$ and that $\phi(\vec{x},\alpha,\sigma)$. We must prove
$F(\vec{x},do(a,s))$, or equivalently, by $F$'s successor state axiom, that
$\phi(\vec{x},a,s) \lor F(\vec{x},s).$\\
{\em Case 1:} $do(\alpha,\sigma) =
do(a,s)$. Then by the unique names axiom for situations, $\alpha = a$ and
$\sigma = s$, and we are done.\\
{\em Case 2:} $do(\alpha,\sigma) <
do(a,s)$. Then by the foundational axioms, $do(\alpha,\sigma) \leq s$, so by
the induction hypothesis, we have $F(\vec{x},s).$
\end{proof}

\begin{corollary}
\label{corollary1}
Let $P$ be a program, and $\cal D$ its action theory. Then, for any fluent $F$,
\[
{\cal D}\models (\forall {\vec x})(\forall s,s').
[F(\vec{x},s)\land s \leq s']
 \supset F(\vec{x},s').
\]
\end{corollary}
This informs us that if a fluent ever becomes
true, it will never again become false.
\begin{corollary}
\label{closedform}
Let $P$ be a  program, $\cal D$ its action theory, and
$F$ a fluent.
Suppose the successor state axiom for $F$ in $\cal D$ is of the form
(\ref{eq:succ}). Then $\cal D$ entails the following
{\em closed form solution} for $F$:
\begin{eqnarray}
\align F(\vec{x},s)\equiv \{ (\exists s')(do(A_1(\vec{x}),s')\leq s
 \land (\exists \vec{y_1})G_1[s'])\lor\cdots\lor \nonumber\\
\align\hspace{4.8em} (\exists s') (do(A_n(\vec{x}),s')\leq s
 \land (\exists \vec{y_n})G_n[s'])\}.
\label{eq:closedform}
\end{eqnarray}
\end{corollary}

\comment{
Corollary \ref{closedform}
gives a {\em closed form
solution}
for each fluent. It will be used to relate our semantics to Clark's completion.
}
Intuitively, this closed form solution (\ref{eq:closedform}) for $F$ says
that
$F$ holds in some situation $s$
iff there is an earlier situation $s'$ in which an action occurs that causes $F$
to be true.
\comment{
In particular, from this proposition, we have
\[
F(\vec{x},s)\supset (\exists s')\{ s'< s
 \land ((\exists \vec{y_1})G_1[s']\lor\cdots\lor
 (\exists \vec{y_n})G_n[s'])\}.
\]
This result will be used later in Section~\ref{equivalence} for
proving equivalences between logic programs.
}

\begin{definition}
\label{definition}
Let $P$ be a  program, and $G$ a goal. A substitution $\sigma$, not necessarily
ground,
is an {\em answer} for $G$ iff 
\[ {\cal D}\models (\forall {\vec x})(\exists s) G\sigma [s],\]
where $G\sigma$ is
the result of simultaneously substituting for variables in $G$ according to
$\sigma$, and $\vec x$ are all the free variables mentioned in $ G\sigma$.
\end{definition}
Therefore query answering in logic programs literally becomes
planning in the style of (Green \cite{Green69}) in the situation calculus.

As we can see from this definition of an answer,
we are primarily interested
in consequences of the form $(\exists s)G[s]$. One nice property about
these consequences of action theories is that they commute over conjunctions:

\begin{proposition}
\label{proposition2}
Let $P$ be a program, and ${\cal D}$ its action theory. For any goals
$G_1$ and $G_2$, whose free variables together are $\vec x$,
$${\cal D}\models (\forall \vec{x})\{
(\exists s)(G_1\;\& \;  G_2)[s] \equiv (\exists s)G_1[s]\land
 (\exists s)G_2[s]\}.
$$
\end{proposition}
\begin{proof}
First, define a function $f$ as follows:
$$
f(s,S_0) = s,
$$
$$
f(s,do(a,s')) = do(a,f(s,s')).
$$
Intuitively, $f(s,s')$ is that situation reached by performing those actions
which took you from $S_0$ to $s$, followed by those actions which took
you from $S_0$ to $s'$.
Next, we prove two lemmas:
\begin{lemma}
For every fluent $F$,
$$
{\cal D} \models (\forall \vec{x},s,s').F(\vec{x},s) \supset F(\vec{x},f(s,s')).
$$
\end{lemma}
Proof of Lemma:\\
The proof is by induction on $s'$, using the induction axiom in the foundational
axioms of the situation calculus.
The case $s' = S_0$ is trivial. Assume the induction hypothesis for $s'$; we
prove, for each fluent $F$, that
$$
(\forall \vec{x},s).F(\vec{x},s) \supset (\forall a)F(\vec{x},f(s,do(a,s'))).
$$
By the definition of $f$, this is equivalent to proving
$$
(\forall \vec{x},s).F(\vec{x},s) \supset (\forall a)F(\vec{x},do(a,f(s,s'))).
$$
By (\ref{eq:succ}), $F$'s successor state axiom has the form 
$F(\vec{x},do(a,s)) \equiv
F(\vec{x},s) \lor \phi(\vec{x},a,s)$. 
Using this and the induction hypothesis, the result follows.

\begin{lemma}
For every fluent $F$,
$$
{\cal D} \models (\forall \vec{x},s,s').F(\vec{x},s) \supset F(\vec{x},f(s',s)).
$$
\end{lemma}
Proof of Lemma:\\
The proof is by induction on $s$. 
As induction hypothesis we take:
$$
(\forall s).\bigwedge[(\forall \vec{x},s').F(\vec{x},s)
\supset F(\vec{x},f(s',s))],
$$
where the conjunction is over the finitely many fluents $F$ of our situation
calculus language.
When $s = S_0$, we must prove:
$(\forall \vec{x},s').F(\vec{x},S_0)
\supset F(\vec{x},s')$. This follows from Corollary \ref{corollary1}. 
Assume the induction hypothesis for $s$; we
prove, for each fluent $F$, that
$$
(\forall \vec{x},a,s').F(\vec{x},do(a,s)) \supset F(\vec{x},f(s',do(a,s))).
$$
By the definition of $f$, this is equivalent to proving
$$
(\forall \vec{x},a,s').F(\vec{x},do(a,s)) \supset F(\vec{x},do(a,f(s',s))).
$$
By $F$'s successor state axiom (\ref{eq:succ}),
$F(\vec{x},do(a,s)) \equiv
F(\vec{x},s) \lor \phi(\vec{x},a,s)$, where $\phi$ is a disjunction
of formulas of the form $(\exists \vec{y}) G[s]\land
a=A(\vec{x})$.
So we must prove
$$
(\forall \vec{x},a,s'). F(\vec{x},s) \lor \phi(\vec{x},a,s) \supset
F(\vec{x},f(s',s)) \lor \phi(\vec{x},a,f(s',s)).
$$
By the induction hypothesis, this simplifies to proving
$$
(\forall \vec{x},a,s').\phi(\vec{x},a,s) \supset
F(\vec{x},f(s',s)) \lor \phi(\vec{x},a,f(s',s)).
$$
Now $\phi(\vec{x},a,s)$ is a disjunction
of formulas of the form $(\exists \vec{y}) G[s]\land
a=A(\vec{x})$, where $G$ is a goal. Hence, by the induction hypothesis,
$$
(\forall \vec{x},a,s').\phi(\vec{x},a,s) \supset
\phi(\vec{x},a,f(s',s)).
$$
This completes the proof of the lemma.

Now, to prove the proposition, notice first that by the properties of
first order logic, the following is valid:
$$
(\forall \vec{x})\{(\exists s)(G_1 \;\& \; G_2)[s] 
\supset (\exists s)G_1[s] \wedge (\exists s)G_2[s]\}.
$$
To prove that 
$$ {\cal D}\models (\forall \vec{x})\{(\exists s)G_1[s]\land
 (\exists s)G_2[s] \supset (\exists s)(G_1\&  G_2)[s]\},
$$
it is sufficient, with no loss of generality, to show that for any two
fluents $F$ and $F'$,
$$ {\cal D}\models (\forall \vec{x},\vec{y})\{(\exists s)F(\vec{x},s) \land
 (\exists s)F'(\vec{y},s) \supset (\exists s)[F(\vec{x},s) 
\land F'(\vec{y},s)]\}. 
$$
To prove this, assume $(\exists s)F(\vec{X},s)$ and $(\exists s)F'(\vec{Y},s)$
for vectors $\vec X$ and $\vec Y$ of Skolem constants. 
Then for constants
$\sigma$ and $\sigma'$, we have
$F(\vec{X},\sigma)$ and $F'(\vec{Y},\sigma')$. 
We must prove 
\begin{equation}
\label{toprove}
(\exists s)[F(\vec{X},s) 
\land F'(\vec{Y},s)]. 
\end{equation}
By Lemma 1, we have $F(\vec{X},f(\sigma,\sigma'))$.
By Lemma 2, we have $F'(\vec{Y},f(\sigma,\sigma'))$.
By taking $s = f(\sigma,\sigma')$ we have proved (\ref{toprove}).
\end{proof}


By Corollary~\ref{closedform} and Proposition \ref{proposition2},
we see that for every
program $P$,
the action theory for $P$ entails
the Clark completion of $P$ with every atom $F(\vec{t})$ replaced by
$(\exists s)F(\vec{t},s)$:

\begin{theorem}
\label{clarkcompletion}
Let $P$ be a  program, $\cal D$ its action theory, and $F$
a fluent. Suppose the successor state axiom for $F$ in $\cal D$ is 
(\ref{eq:succ}), and
$G_i$ is $l_{i1}$ \& $\cdots$ \& $l_{ik_i}$ for $1\leq i\leq n$.
Then $\cal D$ entails the Clark completion for $F$:
\begin{eqnarray*}
\align (\exists s)F(\vec{x},s)\equiv 
 \{ (\exists \vec{y_1})\{
 (\exists s)l_{11}[s]\land\cdots\land (\exists s)l_{1k_1}[s]\}
 \lor\cdots\lor \\
\align\hspace{6.5em} (\exists \vec{y_n})\{(\exists s) l_{n1}[s]\land\cdots\land
 (\exists s)l_{nk_n}[s]\}\}.
\end{eqnarray*}
\end{theorem}


\begin{example}
Consider the logic program $P_1$ with the single rule 
\begin{lprule}
F :- not F
\end{lprule}
By Theorem~\ref{clarkcompletion}, $P_1$'s action theory entails
\[ (\exists s)F(s)\equiv \neg (\exists s)F(s),\]
an inconsistent sentence. Thus the basic action theory for $P_1$ is
inconsistent.

Consider the logic program $P_2$ with the following two rules:
\begin{lprule}
F :- not Q\\
Q :- not F
\end{lprule}
Theorem~\ref{clarkcompletion} yields the following entailment of $P_2$'s
action theory:
\[
(\exists s)F(s) \equiv \neg (\exists s)Q(s).
\]
Thus we can distinguish two classes of models of the action theory for
$P_2$, one in which $\neg (\exists s)Q(s)$ holds so the first rule
is applicable
but not the second, and the other in which  $\neg (\exists s)F(s)$ 
holds so the second rule
is applicable, but not the first.

Now consider the following logic program:\footnote{Thanks to Vladimir Lifschitz
for suggesting this example.}
\begin{lprule}
F :- not Q\\
Q :- not F\\
R :- F\\
R :- Q
\end{lprule}
We prove that $R$ is an answer to this program, which is to say, that
$(\exists s)R(s)$ is an entailment of our situation calculus semantics. By 
Theorem~\ref{clarkcompletion}, this program's action theory entails the 
following Clark completion:
$$
(\exists s)F(s) \equiv \neg (\exists s')Q(s'),
$$
$$
(\exists s)Q(s) \equiv \neg (\exists s')F(s'),
$$
$$
(\exists s)R(s) \equiv (\exists s)F(s) \vee (\exists s)Q(s).
$$
These first order sentences entail $(\exists s)R(s)$, so that $R$ is an
answer to this program.
\end{example}

When there is recursion, our action theory may be stronger than Clark's
completion, as the following example shows.

\begin{example}
\label{example}
Consider the definite program $P_1$ with the following clauses:
\begin{lprule}
ancestor(x,y) :- parent(x,y)\\
ancestor(x,y) :- ancestor(x,z) \& ancestor(z,y)\\
parent(x,y) :- x=John \& y=Joe\\
parent(x,y) :- x=Joe \& y=Bill\\
parent(x,y) :- x=Joe \& y=Susan
\end{lprule}
Let $A_1(x,y),A_2(x,y),B_1(x,y),B_2(x,y),B_3(x,y)$ be the
actions naming these five clauses,
respectively. For the fluent $ancestor$, we have the following two effect
axioms:
\begin{eqnarray*}
\align parent(x,y,s)\land a=A_1(x,y)\supset ancestor(x,y,do(a,s)),\\
\align (\exists z)[ancestor(x,z,s)\land ancestor(z,y,s)]\land a=A_2(x,y)
 \supset\\
\align\hspace{2em} ancestor(x,y,do(a,s)).
\end{eqnarray*}
Thus we have the following successor state axiom for $ancestor$:
\begin{eqnarray*}
\align ancestor(x,y,do(a,s))\equiv \{ a=A_1(x,y)\land parent(x,y,s)\lor\\
\align\hspace{2em} a=A_2(x,y)\land (\exists z). ancestor(x,z,s)\land
 ancestor(z,y,s) \lor\\
\align\hspace{2em} ancestor(x,y,s)\}.
\end{eqnarray*}
Similarly, 
we obtain the following successor state axiom for $parent$:
\begin{eqnarray*}
\align parent(x,y,do(a,s))\equiv \{ x=John\land y=Joe\land a=B_1(x,y)\lor\\
\align\hspace{6em}  x=Joe\land y=Bill\land a=B_2(x,y)\lor\\
\align\hspace{6em} x=Joe\land y=Susan\land a=B_3(x,y)\lor\\
\align\hspace{6em} parent(x,y,s)\}.
\end{eqnarray*}
Let ${\cal D}_1$ be the action theory for $P_1$. By
Theorem~\ref{clarkcompletion}, we have:
\begin{eqnarray*}
\align {\cal D}_1\models (\forall x,y)\{ (\exists s)parent(x,y,s)\equiv
 [(x=John\land y=Joe)\lor\\
\align \hspace{3em} (x=Joe\land y=Bill)\lor
(x=Joe\land y=Susan)]\}.
\end{eqnarray*}
For $ancestor$, Theorem~\ref{clarkcompletion} yields
\begin{eqnarray*}
\align {\cal D}_1\models (\forall x,y)\{(\exists s)ancestor(x,y,s)\equiv
 [(\exists s)parent(x,y,s)\lor\\
\align\tab\tab (\exists z).(\exists s)ancestor(x,z,s)\land (\exists s)ancestor(z,y,s)]\}.
\end{eqnarray*}
This is too weak to give a solution for $ancestor$ (because of the recursion).
However, by the successor state axioms in ${\cal D}_1$, 
using induction on situations (Section 2.2), we can show that
\begin{eqnarray*}
\align {\cal D}_1\models (\forall x,y)\{ (\exists s)ancestor(x,y,s)\equiv
 [(x=John\land y=Joe)\lor\\
\align \hspace{4em} (x=Joe\land y=Bill)\lor
(x=Joe\land y=Susan)\lor\\
\align\hspace{4em} (x=John\land y=Bill)\lor
(x=John\land y=Susan)]\}.
\end{eqnarray*}
This shows that our semantics is strictly stronger than Clark's completion.

Now consider the program $P_2$ which is $P_1$ together with the following
clauses:
\begin{lprule}
childless(x) :- not haschild(x)\\
haschild(x) :- parent(x,y)
\end{lprule}
Let $C(x)$ and $D(x)$ be the corresponding two actions. The successor
state axioms for $parent$ and $ancestor$ with respect to $P_2$ are the same
as those with respect to $P_1$. The successor state axioms for $childless$ and
$haschild$ are:
\begin{eqnarray*}
\align childless(x,do(a,s))\equiv [a=C(x)\land 
 \neg (\exists s')haschild(x,s')\lor\\
\align\hspace{8em} childless(x,s)],\\[1ex]
\align haschild(x,do(a,s))\equiv [a=D(x) \land (\exists y)parent(x,y,s)
 \lor\\
\align\hspace{8em} haschild(x,s)].
\end{eqnarray*}
Let ${\cal D}_2$ be the action theory for $P_2$. By 
Theorem~\ref{clarkcompletion},
we have
\begin{eqnarray*}
\align  {\cal D}_2\models (\forall x).(\exists s)childless(x,s)\equiv
 \neg (\exists  s)haschild(x,s)\\
\align \hspace{1.2in}\equiv 
 \neg (\exists  s)(\exists y)parent(x,y,s)\\
\align \hspace{1.2in}\equiv \neg (x=John\lor x=Joe).
\end{eqnarray*}
\end{example}

In the next section, we shall show that our action theory semantics for logic
programs is closely related to a recent semantics proposed by 
Wallace~\cite{Wallace93}, and is essentially the same as the stable
model semantics \cite{GelfondLifschitz88} when we consider only 
Herbrand models.

\section{Wallace's Semantics}

Wallace's basic idea \cite{Wallace93} can be summarized as follows:
Given a logic program $P$, first
obtain from $P$ another program $P'$, then consider the semantics
of $P$ to be the Clark completion of $P'$.
Wallace proposes several ways for obtaining the new program $P'$ from $P$.
We shall consider the one that is most closely related to our semantics, and
that will in turn relate our semantics to the stable model semantics of
\cite{GelfondLifschitz88}.

The following definition is adapted from \cite{Wallace93}.
Let $P$ be a logic program. The
{\em tightened} program $P'$ of $P$ contains
precisely the following clauses: 
\begin{enumerate}
\item For each clause
\begin{lprule}
$F(\vec{x})$ :- $l_1$ \& $\cdots$ \& $l_n$
\end{lprule}
in $P$, $P'$ contains the clause
\begin{lprule}
$F(\vec{x}, s(n))$ :- $l_1'$ \& $\cdots$ \& $l_k'$
\end{lprule}
where $s(n)$ denotes the successor of the natural number $n$, and
if $l_i=G(\vec{t})$ is an atom, then $l_i'$ is $G(\vec{t},n)$;
if $l_i$ is a negative atom, then $l_i'=l_i$.
\item For each predicate $F(\vec{x})$ in
$P$, $P'$ contains the clause:
\begin{lprule}
$F(\vec{x})$ :- $F(\vec{x},n)$
\end{lprule}
\end{enumerate}
For example, consider the following program adapted from \cite{Wallace93}:
\begin{lprule}
$F(x)$ :- $Q(x)$ \& not $R(x)$\\
$Q(a)$ :-\\
$R(x)$ :- $R(x)$
\end{lprule}
The tightened version of this program is:
\begin{lprule}
$F(x,s(n))$ :- $Q(x,n)$ \& not $R(x)$\\
$Q(a,s(n))$ :-\\
$R(x,s(n))$ :- $R(x,n)$\\
$F(x)$ :- $F(x,n)$\\
$Q(x)$ :- $Q(x,n)$\\
$R(x)$ :- $R(x,n)$\\
\end{lprule}
Notice that the Clark completion of the tightened program yields,
for example, the following completion axiom for $F(x)$:
\[
(\forall x)(F(x) \equiv (\exists n)F(x,n)),
\]
and the following completion axiom for $F(x,n)$:
\[
(\forall x,n)( F(x,n)\equiv (\exists n')(n=s(n')\land Q(x,n'))\land \neg R(x)).
\]
Notice the similarity between this axiom and our successor state axiom for
the fluent $F$, in particular, when $R(x)$ in the above axiom is replaced
by $(\exists n')R(x,n')$ according to the completion of $R(x)$. The differences
are that instead of situations, Wallace uses natural numbers, and instead of
actions and the function $do$, Wallace uses the successor function.

We assume that $0$ is a constant symbol denoting the number zero. So the 
Herbrand models of the Clark completion of tightened programs contains
precisely the following terms about numbers:
\[ 0,s(0), s(s(0)), ...\]

\begin{theorem}
\label{wallace}
Let $P$ be a logic program, $\cal D$ its action theory, and $\cal C$ 
the Clark completion of the tightened version of $P$. Then,
\begin{enumerate}
\item If $M$ is a Herbrand model of $\cal C$, then there is a Herbrand model
$M'$ of $\cal D$ such that for any predicate $F$ in $P$, and any tuple
of Herbrand terms $\vec{t}$,
\[ M\models (\exists n)F(\vec{t},n) \Leftrightarrow
 M'\models (\exists s)F(\vec{t},s).
\]
\item If $M$ is a Herbrand model of $\cal D$, then there is a Herbrand model
$M'$ of $\cal C$ such that for any predicate $F$ in $P$, and any tuple
of Herbrand terms $\vec{t}$,
\[ M\models (\exists s)F(\vec{t},s) \Leftrightarrow
 M'\models (\exists n)F(\vec{t},n).
\]
\end{enumerate}
\end{theorem}
\begin{proof}
First, notice that the Herbrand domain for situations is
\[ \{ S_0, do(\alpha_1,S_0), do(\alpha_2,S_0), ..., do(\alpha_1,do(\alpha_1,S_0)), 
do(\alpha_2,do(\alpha_1,S_0)), ...\}.\]
So any Herbrand interpretation will satisfy the foundational axioms $\Sigma$
of the situation calculus (Section \ref{sitcalc}).

Let $M$ be a Herbrand model of $\cal C$. Construct a Herbrand interpretation
$M'$ with respect to $\cal D$ as follows. For any fluent $F$, let
\begin{enumerate}
\item $M'\models (\forall \vec{x})\neg F(\vec{x},S_0)$.
\item Inductively, 
for any situation term $do(\alpha,S)$, and any tuple of Herbrand terms $\vec{t}$, if
$\alpha$ does not name any clause with $F$ as its head in $P$, then
\[ M'\models F(\vec{t},do(\alpha,S)) \Leftrightarrow M'\models F(\vec{t},S),
\]
and if $\alpha$ names a clause with $F$ as its head, say 
\begin{lprule}
$F(\vec{x})$ :- $F_1(\vec{t_1})$ \& not $F_2(\vec{t_2})$
\end{lprule}
in $P$, then $M'\models F(\vec{t},do(\alpha,S))$ iff 
for some tuple $\vec{u}$ of Herbrand terms of the same length as $\vec{y}$,
the tuple of variables in the above clause but not in
$\vec{x}$,
$M'\models F_1(\vec{t_1},S)(\vec{x},\vec{y}/\vec{t},\vec{u})$ and 
$M\models \neg (\exists n)F_2(\vec{t_2},n)(\vec{x},\vec{y}/\vec{t},\vec{u})$,
where
$F_1(\vec{t_1},S)(\vec{x},\vec{y}/\vec{t},\vec{u})$ is obtained from 
$F_1(\vec{t_1},S)$ by replacing $x_i$ in
$\vec{x} = (x_1,\ldots,x_n)$ by 
the corresponding term $t_i$ in $\vec{t}$, and $y_i$ in $\vec{y}$
by the corresponding term in $\vec{u}$. Similarly for
$F_2(\vec{t_2},n)(\vec{x},\vec{y}/\vec{t},\vec{u})$.
\end{enumerate}
It remains to show that 
\begin{enumerate}
\item $M'$ is a model of $\cal D$.
\item For any fluent $F$, and any tuples of Herbrand terms $\vec{t}$,
\[ M\models (\exists n)F(\vec{t},n) \Leftrightarrow
 M'\models (\exists s)F(\vec{t},s).
\]
\end{enumerate}
Notice that by our construction of $M'$, (1) follows straightforwardly from
(2). To prove the ``$\Rightarrow$'' part of
(2), suppose that for some natural number $N$,
$M\models F(\vec{t},N)$. We show by induction on $N$ that there is a situation
$S$ such that $M'\models F(\vec{t},S)$. The case for $N=0$ is vacuous because
$M\models \neg F(\vec{t},0)$. Inductively, suppose this is true for any 
predicate $F'$, and any $N< K$. Suppose now $M\models F(\vec{t},K)$.
Then since $M$ is a model of the Clark completion of the tightened version of
$P$, there must be a clause with $F$ as its head, say
\begin{lprule}
$F(\vec{x})$ :- $F_1(\vec{t_1})$ \& not $F_2(\vec{t_2})$
\end{lprule}
in $P$ such that 
for some tuple $\vec{u}$ of Herbrand terms of the same length as $\vec{y}$,
the tuple of variables in the above clause, but different from those in
$\vec{x}$,
\[ M\models F_1(\vec{t_1},K-1)(\vec{x},\vec{y}/\vec{t},\vec{u})\land 
\neg (\exists n) F_2(\vec{t_2},n)(\vec{x},\vec{y}/\vec{t},\vec{u}).
\]
By the inductive assumption, there is a situation $S_1$ such that
$M'\models  F_1(\vec{t_1},S_1)(\vec{x},\vec{y}/\vec{t},\vec{u})$.
Now let $A(\vec{x})$ be the action naming the above clause for $F$.
By the construction of $M'$, we have that
$M'\models F(\vec{t},do(A(\vec{t}),S_1))$. 
This completes the inductive step, thus 
the ``$\Rightarrow$'' part of (2). The ``$\Leftarrow$'' part of (2) can be
proved similarly by doing induction on situations.

This completes the proof for the first half of the theorem. The proof
of the second half is similar. 
\end{proof}

>From this theorem and Theorem 8 in \cite{Wallace93} that relates Wallace's
semantics to the stable model semantics, we have:

\begin{corollary}
\label{stable}
Let $P$ be a program, and $\cal D$ its action theory.
A set $\cal S$ of ground atoms is a stable model of $P$ iff there is a Herbrand
model $M$ of $\cal D$ such that for any ground atom $F(\vec{t})$, 
$F(\vec{t})\in\cal S$ iff
$M\models (\exists s)F(\vec{t},s)$.
\end{corollary}

For any logic program $P$, Wallace also defines
the {\em full completion} of $P$ to be the
Clark completion of the tightened version of $P$ together with appropriate
induction axioms for natural numbers,
and shows that
for any ground atom $p$, $p$ is entailed by the full completion iff it
is in the {\em success set} of the tight tree
semantics of $P$ as defined in
(van Gelder \cite{vanGelder89}), and $\neg p$ is entailed by the full
completion iff $p$ is in the {\em finite failure set} of $P$.
Since our foundational axioms in $\Sigma$ already include an induction axiom,
this result carries over to our semantics as well.

Wallace~\cite{Wallace93} also relates his semantics to some other well-known
ones such as
(Fitting~\cite{Fitting85}, 
Kunen~\cite{Kunen87}, Przymusinski~\cite{Przymusinski88}, 
and
van Gelder and Ross and Schlipf~\cite{VanGelder88}).
Many of the results there can be inherited here. Wallace also
argues the advantages of
having a semantics in first-order logic. The same arguments apply to 
our semantics as well.

Admittedly, compared to Wallace's elegant approach, ours seems 
complicated. However, there are some important reasons for
appealing to actions and their axiomatization within the situation calculus.
\begin{enumerate}
\item Appealing to theories of actions as they are normally understood in
artificial intelligence reveals the connection between the 
classical frame problem
and the semantics for negation-as-failure.
\item By treating rule applications as first-order objects, we can
formally reason about them within the situation calculus.
This becomes important when we come to
formalize search control operators in logic programming.
Because actions and situations are first order terms, and because a
situation denotes
the sequence of actions (history) that have occurred thus far, a situation
in our logic programming semantics is a record of {\em all the derivations that
have been performed thus far, in the order in which they have been
performed}.
To date, most formal analyses of logic programming
have ignored their ``dirty aspects'' like
the cut operator. In essence, these operators place certain constraints on
reachable situations, i.e. on the permitted derivation histories. 
These conditions are normally rather complicated
and require the ability to talk formally about derivation histories, which
our situation calculus-based semantics does provide. We shall 
say more about this issue in Section \ref{other} below.
\end{enumerate}

Technically, this paper also goes beyond that of (Wallace \cite{Wallace93})
in defining an equivalence relation on logic programs, and
proving conditions for two
logic programs to be equivalent. This is the goal of the next section.



\section{Program Transformations}
\label{equivalence}

One reason for a formal semantics of a programming 
language is to study sound program transformation techniques.
To this end,
we first need a notion
of equivalence between two logic programs. 

\subsection{An Equivalence Relation}

Let $P$ and $P'$ be two programs,
and ${\cal D}$ and ${\cal D}'$ their respective action theories.
Normally ${\cal D}$ and ${\cal D}'$ will not be compatible. For example,
any action in $P$ but not in $P'$ will have no effect according to ${\cal D}'$.
Given our definition of answers to queries, it is natural then to say that
$P$ and $P'$ are equivalent iff they give the same answer to every query,
i.e., for any goal $G$, ${\cal D}\models (\exists s)G[s]$ iff
${\cal D}'\models (\exists s)G[s]$. However, this definition does not seem
to be fine-grained enough. For example, the following program
\begin{lprule}
F :- not Q\\
Q :- not F\\
R :- F
\end{lprule}
gives the same answer to every query as the following one:
\begin{lprule}
F :- not Q\\
Q :- not F\\
R :- Q
\end{lprule}
But intuitively, we don't want them to be equivalent because there is
a model of the action theory of the first program in which 
\[
\neg (\exists s)Q(s)\land (\exists s)F(s)\land (\exists s)R(s)
\]
holds, but there is no model of the action theory of the second program
that satisfies this sentence.\footnote{Notice that
the set of stable models for the first program is 
$\{ \{ F,R\},\{ Q\}\}$, but for the second program it is
$\{ \{ Q,R\},\{ F\}\}$. So these two programs are not equivalent
in terms of their stable model semantics. Later we shall show that in the
propositional case, our
notion of equivalence coincides with that under the stable model semantics.}
This suggests that we should define program
equivalence model-theoretically.

Let $P$ be a logic program, $\cal D$ its action theory. We call a
theory $T$ an {\em answer theory} of $P$ iff for every structure $M$,
$M$ is a model of $T$ iff there is a model $M'$ of $\cal D$ such that
$M$ and $M'$ agree on $(\exists s)G[s]$, for any goal $G$.
In the following, we write this agreement relation as
$M\sim M'$. Formally, $M\sim M'$ iff
\begin{enumerate}
\setlength{\itemsep}{0.0pt}
\item $M$ and $M'$ have the same domain for sort 
{\em object}. Recall that this is the sort for entities other than actions
and situations.
\item For any goal $G$, and any variable assignment $\sigma$,\footnote{$M,\sigma\models (\exists s)G[s]$
means that the formula $(\exists s)G[s]$ is true under the variable assignment
$\sigma$ in $M$.}
\[ M,\sigma\models (\exists s)G[s] \mbox{ iff }
M',\sigma\models (\exists s)G[s].
\]
\end{enumerate}
It is clear that if both $T$ and $T'$ are answer theories of $P$, then
$T$ and $T'$ are logically equivalent. So if $T$ is an answer theory of
$P$, then we can say that $T$ is {\em the} answer theory. 

Notice that by Proposition~\ref{proposition2}, condition 2 holds for
arbitrary $(\exists s)G[s]$ iff it holds for any 
$(\exists s)F(\vec{x},s)$,
where $F$ is a fluent:
\begin{proposition}
\label{fluentequiv}
$M\sim M'$ iff
\begin{enumerate}
\setlength{\itemsep}{0.0pt}
\item $M$ and $M'$ have the same domain for sort
{\em object}. 
\item For any fluent $F$, and any variable assignment $\sigma$,
\[ M,\sigma\models (\exists s)F(\vec{x},s) \mbox{ iff }
M',\sigma\models (\exists s)F(\vec{x},s).
\]
\end{enumerate}
\end{proposition}

It turns out that the answer
theory of $P$ can be considered to be the result of {\em remembering only}
$(\exists s)F(\vec{x},s)$, for every fluent $F$
in $\cal D$ (Lin and Reiter \cite{LinReiter:forgetting}). Moreover,
according to
the results in (Lin and Reiter \cite{LinReiter:forgetting}), 
the answer theory of $P$ always exists, and
can be expressed as a finite second-order theory, but that in general, no
first-order answer theory need exist.

We now have the following definition:\footnote{We remark here that 
equivalence between two programs under Wallace's semantics 
\cite{Wallace93} can be  similarly defined.}

\begin{definition}
Two logic programs $P$ and $P'$ are {\em equivalent} iff 
their answer theories are logically equivalent.
\end{definition}

\begin{example}
Consider again the two programs given earlier in this section. The
answer theories for these two programs happen to be their respective
Clark completions. The first answer theory is
\begin{eqnarray*}
&& (\exists s)F(s)\equiv \neg (\exists s)Q(s)\land \\
&& (\exists s)R(s)\equiv (\exists s)F(s).
\end{eqnarray*}
The second answer theory is
\begin{eqnarray*}
&& (\exists s)F(s)\equiv \neg (\exists s)Q(s)\land \\
&& (\exists s)R(s)\equiv (\exists s)Q(s).
\end{eqnarray*}
These two theories are not equivalent.
\end{example}

According to Corollary~\ref{stable} that relates our semantics to the
stable model semantics, we see, by virtue of Proposition \ref{fluentequiv},
that a stable model of a logic
program $P$ is a Herbrand model (in the sense of Corollary~\ref{stable})
of its answer theory. In particular, in the propositional case, the answer
theory of a logic program is simply the disjunction of its stable models;
and two programs $P$ and $P'$ are equivalent iff 
their stable models are the same:

\begin{proposition}
\label{stable1}
Let $P$ and $P'$ be two propositional logic programs.
\begin{enumerate}
\item A theory $T$ is the answer theory of $P$ iff the set of models 
of $T$ equals the set of stable models of $P$.
\item $P$ and $P'$ are equivalent iff the set of 
stable models of $P$ equals the set of stable models of $P'$.
\end{enumerate}
\end{proposition}

The following proposition is straightforward:

\begin{proposition}
\label{prop:equivalence}
Let $P$ and $P'$ be two logic programs, and $\cal D$ and ${\cal D}'$ their
respective action theories. The answer theory of $P$ entails that of $P'$
iff for any model $M$ of $\cal D$, there is a model of $M'$ of
${\cal D}'$ such that $M\sim M'$.
\end{proposition}

\subsection{Equivalence of Definite Logic Programs}

A logic program is {\em definite} if it does not mention any negative
atoms
in any of its clauses.
The conditions for two definite programs to be equivalent are just as one
would expect: $P$ and $P'$ are equivalent iff $P$ entails each clause
in $P'$ and vice versa. In our language, we have:

\begin{theorem}
\label{positive}
Let $P$ and $P'$ be two definite logic programs, 
and $\cal D$ and ${\cal D}'$ their
action theories. 
$P$ and $P'$ are equivalent if and only if the following two conditions hold:
\begin{enumerate}
\setlength{\itemsep}{0pt}
\item For every clause $F(\vec{x})\mbox{ \tt :- } G$
in $P'$,
\begin{equation}
\label{eq:thm1}
{\cal D}\models (\forall \vec{x}).  (\exists \vec{y}, s)G[s]\supset
 (\exists s)F(\vec x,s),
\end{equation}
where $\vec{y}$ is the tuple of those variables in $G$ but not in $\vec{x}$.
\item Symmetrically, for every clause $F(\vec{x})\mbox{ \tt :- } G$
in $P$,
\begin{equation}
\label{eq:thm2}
{\cal D}'\models (\forall \vec{x}). (\exists \vec{y},s)G[s]\supset 
(\exists s)F(\vec{x},s).
\end{equation}
\end{enumerate}
\end{theorem}
\begin{proof}
The ``only if'' follows directly from the definition. We show the ``if''
part.

Given any definite logic program $P_1$, and any model $M$ of 
$\Sigma\cup {\cal D}_{una}$, there is a ``unique'' way of transforming
$M$ into
a model of the action theory of $P_1$. Briefly, this is done as follows.
Let $M'$ agree with $M$ on everything except possibly on their interpretations
of fluents. (So in particular, $M$ and $M'$ share the same domain 
for every sort.)
Then $M'$ is also a model of $\Sigma\cup {\cal D}_{una}$. 

For any fluent $F(\vec{x},s)$, let $M'\models (\forall x)\neg F(\vec{x},S_0)$.
Inductively, if
the successor state axiom for $F$ w.r.t. $P_1$ is:
\[
(\forall \vec{x},a,s) F(\vec{x},do(a,s))\equiv \Phi(a,\vec{x},s),
\]
then let
\[
M'\models (\forall \vec{x},a,s) F(\vec{x},do(a,s))\equiv \Phi(a,\vec{x},s).
\]
This is well-defined, because $P_1$ is a definite program, 
so $\Phi(a,\vec{x},s)$
can be evaluated using the truth values of fluents in the situation $s$. In
particular, it does not contain formulas like $(\forall s')F(s')$.
Now it follows directly
from the construction that $M'$ is a model of the action theory for $P_1$. 

Now we show the ``if'' part using Proposition~\ref{prop:equivalence}.
Suppose $M$ is a model of $\cal D$. Let $M'$ be the model of ${\cal D}'$
constructed from $M$ as above. 
We show $M\sim M'$, i.e., by Proposition \ref{fluentequiv}, for any fluent $F$
and any variable assignment $\sigma$, 
\[
M,\sigma\models (\exists s)F(\vec{x},s) \mbox{ iff }
M',\sigma\models (\exists s)F(\vec{x},s).
\]
Suppose
$$
M,\sigma\models F(\vec{x},s).
$$
We show by induction on $s$ that
$M',\sigma\models (\exists s)F(\vec{x},s)$.

The case for $s=S_0$ is trivial. Inductively, suppose that for any fluent,
this is true for $s^*$. 
We show that for any action $\alpha$, this is true for $do(\alpha,s^*)$
as well. 
Since $M$ is a model of $\cal D$, by the form of successor state axioms,
there are two cases:
\begin{enumerate}
\item $M,\sigma\models F(\vec{x},s^*)$.
\item $\alpha$ names one of the clauses in the definition of $F$ in $P$, say
\begin{lprule}
$F(\vec{x})$ :- $F_1(\vec{t_1})$ \& $F_2(\vec{t_2})$
\end{lprule}
and 
\[
M,\sigma\models (\exists\vec{y}). F_1(\vec{t_1},s^*)\land F_2(\vec{t_2},s^*),
\]
where $\vec{y}$ is the tuple of variables mentioned in $\vec{t_1}$ or
$\vec{t_2}$, but not in $\vec{x}$.
\end{enumerate}
In the first case, the result follows from our inductive assumption.
Suppose it is the latter case. By the inductive assumption, we have
\[
M',\sigma\models (\exists \vec{y})[(\exists s')F_1(\vec{t_1},s')\land (\exists s')F_2(\vec{t_2},s')].
\]
But $M'$ is a model of ${\cal D}'$.
So, by the assumption (\ref{eq:thm2}), instantiated to the above clause in $P$,
we have:
\[
M',\sigma\models 
(\exists \vec{y})[(\exists s')F_1(\vec{t_1},s')\land (\exists s')F_2(\vec{t_2},s')]\supset 
 (\exists s')F(\vec{x},s).
\]
Therefore 
\[
M',\sigma\models (\exists s)F(\vec{x},s).
\]
This proves the inductive step. Therefore whenever 
$M,\sigma\models (\exists s)F(\vec{x},s)$, we have
$M',\sigma\models (\exists s)F(\vec{x},s)$. The converse can be proved
similarly. Thus $M\sim M'$.

Symmetrically, if $M\models {\cal D}'$, then there is a model $M'$ of
${\cal D}$ such that $M\sim M'$.

This proves that $P$ and $P'$ are equivalent.
\end{proof}

In principle, checking conditions (\ref{eq:thm1}) and (\ref{eq:thm2})
requires induction. However, there are some sufficient ways to do this that
may be useful in practice. 
To illustrate the
ideas, suppose the program $P'$ contains the following clause:
\begin{lprule}
$F(x)$ :- $x=f(y)$ \& $F'(x,g(y))$
\end{lprule}
and we want to verify (\ref{eq:thm1}) for it.
Let $a$ be a
fresh constant symbol not already mentioned
in $P$ and $P'$. Then one way to do this
is to first add $F'(f(a),g(a))$ to $P$, and then query
the new program with $F(f(a))$.
If the query succeeds, then the condition
holds. However, if the query fails, this does not mean that the
condition is false. For instance, this condition holds trivially when
$P$ is the empty program but $G$ in (\ref{eq:thm1}) has at least
one atom, because when
$P$ is empty, its action theory entails $\neg (\exists s)F(s)$ for 
any fluent $F$. This strategy was first used by Sagiv \cite{Sagiv88}
for proving the equivalence of two deductive databases.

Yet another way to prove condition (\ref{eq:thm1}) say, is to 
query the program  $P$ with
the goal $G$, and then query $P$ again with the goal $F(\vec{x})$
for those bindings returned by the first query.
If the goal $F(\vec{x})$ succeeds for all these bindings, then
condition (\ref{eq:thm1}) holds.
The problem with this strategy is that it may not work when there are
infinitely many bindings for the first query.

Finally, we remark that if condition (\ref{eq:thm1}) holds, then 
${\cal D}'\models (\exists s)F(\vec{t},s)$ implies
${\cal D}\models (\exists s)F(\vec{t},s)$, i.e. the set of ground atoms
provable from $P'$ is a subset of that from $P$. 
However, this does not mean that
the answer theory of $P$ will entail that of $P'$. For the latter to be
true, the set of negative ground atoms provable from $P'$ would have to
be a subset of that from $P$ as well.
In fact, if the answer
theory of a positive program entails that of another positive program,
then these two positive programs must be equivalent. This is because 
for any positive program $P$, the models of the answer theory
$\cal D$ of $P$
must be unique in the sense that if two models of $\cal D$ share the
same domains, then they must be the same.
That in turn is because of the closed world assumption made
in logic programs.


\subsection{Normal Logic Programs}

Unfortunately, Theorem \ref{positive} fails for logic programs with
negation: Suppose the program $P$ consists of the following single clause:
\begin{lprule}
F:- 
\end{lprule}
and the program $P'$ consists of the following single clause:
\begin{lprule}
F :- not F
\end{lprule}
Clearly, $P$ and $P'$ are not equivalent. But
condition (\ref{eq:thm1}), which in this case is
\[
{\cal D}\models \neg (\exists s)F(s)\supset (\exists s)F(s),
\]
holds since ${\cal D}\models (\exists s)F(s)$, and condition
(\ref{eq:thm2}) holds trivially because ${\cal D}'$ in this case is an
inconsistent theory.


%For normal logic programs, we do not have a result like
%Theorem~\ref{positive} for definite programs. 
Intuitively, the
reason Theorem~\ref{positive} works for
%that conditions (\ref{eq:thm1}) and (\ref{eq:thm2}) work for
definite programs is that if $F(s)$ is provable from a definition program,
then there must be a situation $s'$ such that $s'$ is {\em earlier} than
$s$ ($s'< s$), and a goal $G$ such that $G[s']$ is provable and {\em does
not} quantify over situations, i.e. $G[s']$ is a statement whose truth
value can be determined by looking at the situation $s'$ alone. This will
ensure that there are no cycles, and thus induction on situation will
work.
This property is lost on normal logic programs because if $G$ mentions
negation, then $G[s]$ will quantify over situations, and its truth
value will depend on the entire space of situations.
To overcome this, the trick is then to introduce some new situation
independent predicates, and replace formulas of the form 
$(\exists s')F(s')$
in $G[s]$ by atoms made of such new predicates. 
This will make the resulting formula ``look'' like a statement whose
truth value depends only on the situation $s$.
This is exactly the intuition behind the following definitions which will
be used to formulate some sufficient conditions for two normal logic
programs to be equivalent.

Suppose  $P$ is a logic program. For any predicate $F(\vec{x})$ in $P$,
suppose $\new{F}(\vec{x})$ is a new predicate symbol with the same arity as
 $F$.
We define the {\em loosened} action theory $\new{\cal D}$ of
$P$ to be that
obtained 
from $P$'s action theory $\cal D$ by replacing in $\cal D$'s
successor state axioms every subformula of the
form $(\exists s')F(\vec{t},s')$ by $\new{F}(\vec{t})$, for every fluent $F$.
For example, if the successor state axiom for $F$ is
\begin{eqnarray*}
\align F(\vec{x},do(a,s)) \equiv \\
\align\hspace{3em} (\exists \vec{y})[a=A(\vec{x})\land F_1(\vec{t_1},s)\land 
 \neg (\exists s')F_2(\vec{t_2},s')]\lor F(\vec{x},s),
\end{eqnarray*}
then the new axiom, called the {\em loosened} successor state axiom of $F$,
is
\begin{eqnarray*}
\align F(\vec{x},do(a,s)) \equiv \\
\align\hspace{3em} (\exists \vec{y})[a=A(\vec{x})\land F_1(\vec{t_1},s)\land 
 \neg \new{F_2}(\vec{t_2})]\lor F(\vec{x},s).
\end{eqnarray*}

Loosened action theories are like action theories for definite logic programs.
The propositions and theorems in Section~\ref{semantics} can be extended to
them as well. For instance, corresponding to Theorem~\ref{clarkcompletion},
we have: If $(\forall \vec{x}). (\exists s)F(\vec{x},s)\equiv \Phi(\vec{x})$
is the Clark completion of the fluent $F$ in the program $P$, then
\begin{equation}
\label{loosened}
\new{{\cal D}}\models 
 (\forall \vec{x}). (\exists s)F(\vec{x},s)\equiv \Phi'(\vec{x}),
\end{equation}
where $\new{\cal D}$ is the loosened action theory of $P$, and $\Phi'$ is
the result of replacing in $\Phi$ every subformula of the form 
$\neg (\exists s)F'(\vec{t},s)$ by $\new{F'}(\vec{t})$, for every fluent $F'$.


In the following,
we call a formula $\Phi(\vec{x},s)$ a {\em simple state formula} if:
\begin{enumerate}
\item Its free variables are among $\vec{x},s$.
\item It does not mention the initial state $S_0$.
\item It does not quantify over situations.
\item It does not mention $do$, $Poss$, or $<$.
\end{enumerate}
Informally, $\Phi(\vec{x},s)$ is a simple state formula 
when its truth value can be determined
by the truth values of fluents in the situation $s$, and the
truth values of state independent predicates like $\new{F}$ and equality.

\comment{
We see that for any program $P$, any fluent $F$, the loosened
successor state axiom for $F$ w.r.t. $P$ has the form:
$
F(\vec{x},do(a,s))\equiv \Phi_F(\vec{x},a,s)
$,
where
$\Phi_F(\vec{x},a,s)$ is a simple state formula.
}

In the following, we let $\cal F$ be:
\begin{equation}
{\cal F}= \{ (\forall \vec{x})[
 (\exists s)F(\vec{x},s)\equiv \new{F}(\vec{x})]\D \mbox{$F$ is a fluent}\}
\label{new}
\end{equation}

\begin{theorem}
\label{th:equivalence}
Let $P_1$ and $P_2$ be two logic programs and let
${\cal D}_1$ and ${\cal D}_2$ be their respective
action theories.
In addition, let $\new{{\cal D}_2}$ be the loosened action theory of
$P_2$. Finally, suppose
\begin{enumerate}
\setlength{\itemsep}{0pt}
\item For every clause $F(\vec{x})\mbox{ \tt :- } G$
in $P_2$,
\begin{equation}
\label{eq:thm3}
{\cal D}_1\models (\forall \vec{x}). (\exists\vec{y}, s)G[s]\supset
 (\exists s)F(\vec x,s),
\end{equation}
where $\vec{y}$ is the tuple of variables mentioned in $G$ but not in $\vec{x}$.
\item For every fluent $F(\vec{x},s)$, there is a 
simple state formula $\Psi_F(\vec{x},s)$ such that:
\begin{enumerate}
\item In this formula, every fluent appears positively;
\item
\begin{equation}
{\cal D}_1\cup {\cal F}
\models 
(\forall \vec{x}). F(\vec{x},s)\supset 
 (\exists s')(s'< s\land \Psi_F(\vec{x},s'));
\label{eq:thm5}
\end{equation}
\item
\begin{equation}
 \new{{\cal D}_2}\models 
(\forall \vec{x}). \Psi_F'(\vec{x})\supset (\exists s)F(\vec{x},s),
 \label{eq:thm4}
\end{equation}
where $\Psi_F'(\vec{x})$ is the result of replacing every atomic formula
of the form $F'(\vec{t},s)$ in $\Psi_F(\vec{x},s)$ by
$(\exists s)F'(\vec{t},s)$, for every fluent $F'$.
\end{enumerate}
\end{enumerate}
Then the answer theory of $P_1$ entails that of $P_2$.
\end{theorem}
Let us briefly comment on the theorem before proving it. 
Condition (\ref{eq:thm5}) means that if $F(s)$ holds, then there must
be a situation $s'$ {\em earlier} than $s$ such that $\Psi_F(s')$ holds.
Since $\Psi_F$ is a simple state formula, its truth value depends only
on $s'$, so induction on situations will go through. Compared to 
Theorem~\ref{positive}, $\Psi_F$ is like $G$. But since $F\mbox{ :- } G$
is a clause in $P$, condition (\ref{eq:thm5}) always holds for
positive logic programs. Now
condition (\ref{eq:thm4}) is like condition (\ref{eq:thm2}) in 
Theorem~\ref{positive}, with ${\cal D}'$ replaced by $\new{{\cal D}_2}$,
and $G$ by $\Psi_F'$.

\begin{proof}
We need to show that for any model $M_1$ of ${\cal D}_1$, there is a model
$M_2$ of ${\cal D}_2$ such that $M_1\sim M_2$.

Suppose that $M_1$ is a model of ${\cal D}_1$. Since for any fluent $F$,
$\new{F}$ does not appear in ${\cal D}_1$, we can assume that
$M_1$ satisfies $\cal F$ as well.


Construct a first-order structure $M_2$ as
follows:
\begin{enumerate}
\setlength{\itemsep}{0pt}
\item It shares with $M_1$ the domain for every sort.
\item Except possibly on fluents, it shares with $M_1$ the interpretation of
all function and predicate symbols. In particular, they agree on the
new predicates.
\item For every fluent $F$, $M_2\models (\forall \vec{x})\neg F(\vec{x},S_0)$,
and inductively, if
\[
F(\vec{x},do(a,s))\equiv \Phi_F(\vec{x},a,s),
\]
is the loosened successor state axiom of $F$ for $P_2$, then let
\[
M_2\models (\forall \vec{x},a,s)[F(\vec{x},do(a,s))\equiv \Phi_F(\vec{x},a,s)].
\]
Again (cf. the proof of Theorem~\ref{positive}), this is well defined because
$\Phi_F$ is a simple state formula.
\end{enumerate}
Clearly, $M_2$ is a model of $\new{{\cal D}_2}$, the loosened action theory
of $P_2$.

We now show $M_1\sim M_2$, i.e., for any fluent $F$,
and any variable assignment $\sigma$, 
\[
M_1,\sigma\models (\exists s)F(\vec{x},s) \mbox{ iff }
M_2,\sigma\models (\exists s)F(\vec{x},s).
\]
Suppose
$$
M_2,\sigma\models F(\vec{x},s).
$$
We show by induction on $s$ that
$M_1,\sigma\models (\exists s)F(\vec{x},s)$.

The case for $s=S_0$ is trivial. Inductively, suppose that for any fluent,
this is true for $s^*$. 
We show that for any action $\alpha$, this is true for $do(\alpha,s^*)$
as well. By the construction of $M_2$, and the form of successor state
axioms, there are two cases:
\begin{enumerate}
\item $M_2,\sigma\models F(\vec{x},s^*)$.
\item $\alpha$ names one of the clauses in the definition of $F$ in $P'$, say
\begin{lprule}
$F(\vec{x})$ :- $F_1(\vec{t_1})$ \& not $F_2(\vec{t_2})$
\end{lprule}
and
\[
M_2,\sigma\models (\exists \vec{y}).
 F_1(\vec{t_1},s^*)\land \neg \new{F_2}(\vec{t_2}),
\]
where 
$\vec{y}$ is the tuple of variables in $\vec{t_1}$ or
$\vec{t_2}$, but not in $\vec{x}$.
\end{enumerate}
In the first case, the result follows from our inductive assumption.
So consider the latter case. By the inductive assumption, we have
\[
M_1,\sigma\models (\exists \vec{y})[(\exists s')F_1(\vec{t_1},s')\land
 \neg \new{F_2}(\vec{t_2})].
\]
But $M_1$ is a model of the set ${\cal F}$ (\ref{new}), thus
\[
M_1,\sigma\models (\exists \vec{y})[(\exists s')F_1(\vec{t_1},s')\land
 \neg (\exists s')F_2(\vec{t_2},s')].
\]
But the assumption (\ref{eq:thm3}), when instantiated to the above clause,
yields:
\[
M_1,\sigma\models (\exists \vec{y})[(\exists s')F_1(\vec{t_1},s')\land
 \neg (\exists s')F_2(\vec{t_2},s')]\supset (\exists s')F(\vec{x},s').
\]
So we have
\[
M_1,\sigma\models (\exists s)F(\vec{x},s).
\]
This proves the inductive step. Therefore whenever 
$M_2,\sigma\models (\exists s)F(\vec{x},s)$, we have
$M_1,\sigma\models (\exists s)F(\vec{x},s)$.

Now suppose $M_1,\sigma\models F(\vec{x},s)$. We show that
$M_2,\sigma\models (\exists s)F(\vec{x},s)$. 
Again, we do induction on $s$.
The case $S_0$ is vacuous
because the assumption is false. 
Inductively, assume that the result holds for any fluent, for any state
$s< s^*$.
We show that it is true for $s^*$
as well. 
Suppose $M_1,\sigma\models F(\vec{x},s^*)$.
Since $M_1$ is a model of ${\cal D}_1$ and the set (\ref{new}),
by the assumption (\ref{eq:thm5}), we have
\[
M_1,\sigma\models (\exists s)(s< s^*\land \Psi_F(\vec{x},s)).
\]
Now by the inductive assumption, the fact that $M_2$ and $M_1$ agree on
everything else except possibly on fluents,
and the assumption that every fluent appears positively
in $\Psi_F$, we have that
\[
M_2,\sigma\models \Psi_F'(\vec{x})
\]
where $\Psi_F'(\vec{x})$ is as in (\ref{eq:thm4}).
Therefore, by the assumption (\ref{eq:thm4}), we have
\[ M_2,\sigma\models (\exists s)F(\vec{x},s).
\]
This completes the inductive proof.
So we have proved that $M_1\sim M_2$. Using this, the fact that $M_1$ is
a model of the set $\cal F$, and the fact that $M_1$ and $M_2$
agree on all new predicates $\new{F}$, we conclude that $M_2$ is
a model of $\cal F$ (\ref{new}) as well. Thus, by the definition
of the loosened action theory, $M_2$ is a model of  ${\cal D}_2$.
This concludes the proof of the theorem.
\end{proof}

To use Theorem~\ref{th:equivalence}, one needs to select the appropriate
formula $\Psi_F$, for every fluent $F$. The following are some candidates.

Let 
\[
(\exists s)F(\vec{x},s) \equiv \Phi(\vec{x})
\]
be the Clark completion of $F$ (see Theorem~\ref{clarkcompletion}) in $P_2$.
\begin{itemize}
\item Let $\Psi_F(\vec{x},s)$ be
the result of replacing in $\Phi$ every positive subformula of the form
$(\exists s)F'(\vec{t},s)$ by $F'(\vec{t},s)$, and every negative subformula
of the form
$(\exists s)F'(\vec{t}, s)$ by $\new{F'}(\vec{t})$. Then
$\Psi_F$
satisfies the required syntactic conditions: it is a simple state formula, and
every fluent in it appears positively. 
By (\ref{loosened}), it also satisfies the condition
(\ref{eq:thm4}). So condition (\ref{eq:thm5}) is the only
one left to be checked. 
\comment{
Notice that if the Clark completion of $F$
in both $P_1$ and $P_2$ is the same, then, by Corollary~\ref{closedform},
condition (\ref{eq:thm5}) holds for this $\Psi_F$ as well.
}
\item If $\Phi$ has a positive occurrence of 
$(\exists s)F_1(\vec{t},s)$, and
\[
(\exists s)F_1(\vec{x},s) \equiv \Phi_1(\vec{x})
\]
is the Clark completion of $F_1$, then first let $\Phi'$ be the 
result of replacing in $\Phi$ this positive occurrence of
$(\exists s)F_1(\vec{t},s)$ by $\Phi_1(\vec{t})$, and let
$\Psi_F(\vec{x})$ be obtained from $\Phi'$ the same way as it is obtained
from $\Phi$ above.
Then $\Psi_F$ again is a simple state formula, 
every fluent in it appears positively, and satisfies condition
(\ref{eq:thm4}). 
\item The above procedure of obtaining $\Psi_F$ can be iterated.
Notice that this procedure is closely related to
unfolding (see below), and also
{\em regression} \cite{Waldinger77,Pednault88,Reiter91} in planning.
\end{itemize}

For example, given the following Clark completion for $F$:
\[
(\exists s)F(s) \equiv \{ (\exists x, s)F_1(x,s)\lor [
 (\exists s)F_2(s)\land \neg (\exists s)F_3(s)]\}
\]
we obtain the following possible $\Psi_F$:
\[ (\exists x)F_1(x,s)\lor [ F_2(s)\land \neg \new{F_3}]
\]
Now suppose
\[
(\exists s)F_1(x,s)\equiv (\exists s)F_4(x,s)\lor (\exists y)(
(\exists s)F_2(s)\land \neg(\exists s')F_5(x,y,s'))
\]
is the Clark completion of $F_1$.
First eliminate $(\exists s)F_1(x,s)$ in the Clark completion of $F$:
\begin{eqnarray*}
\align
(\exists s)F(s) \equiv \{ (\exists x)[(\exists s)F_4(x,s)\lor (\exists y)(
(\exists s)F_2(s)\land \neg(\exists s')F_5(x,y,s'))]\lor \\
\align\hspace{3em}
 (\exists s)F_2(s)\land \neg (\exists s)F_3(s)\}.
\end{eqnarray*}
>From this, we get another possible $\Psi_F$:
\[
 (\exists x)[F_4(x,s)\lor (\exists y)(
 F_2(s)\land \neg \new{F_5}(x,y))]\lor 
[F_2(s)\land \neg \new{F_3}],\]
which is logically equivalent to
\[
 (\exists x)[F_4(x,s)\land F_2(s)]\lor (\exists x, y)[
 F_4(x,s)\land \neg \new{F_5}(x,y)]\lor 
[F_2(s)\land \neg \new{F_3}].
\]

We further illustrate the use of the theorem by proving
the following simple equivalence:

\begin{proposition}
\label{simpleequiv}
Let $P_1$ be a program, $F_1$ an atom, and $G$ a goal. Let $P_2$
be the union of $P_1$ with the clause:
\begin{lprule}
$F_1$ :- $F_1$ \& $G$
\end{lprule}
Then $P_1$ and $P_2$ are equivalent.
\end{proposition}
\begin{proof}
Suppose the Clark completion for $F_1$ in $P_1$ is
\[
(\exists s)F_1(s)\equiv \Phi
\]
and $\Psi_{F_1}(s)$ is a simple state formula obtained from $\Phi$ as
outlined above.
Then 
the Clark completion for $F_1$ in $P_2$ is of the form:
\begin{equation}
\label{proof10}
(\exists s)F_1(s)\equiv [(\exists s)F_1(s)\land \var]\lor \Phi
\end{equation}

We show that the answer theory of $P_2$ entails that of $P_1$. The converse
is easier, and can be similarly proved.\\[1ex]
{\bf Condition} (\ref{eq:thm3}). Trivial, since every clause in $P_1$ is also
a clause in $P_2$.\\[1ex]
{\bf Conditions} (\ref{eq:thm4}) and (\ref{eq:thm5}).
For each fluent $F$, we use the Clark completion of $F$ in $P_1$ to generate
the formula $\Psi_F$ as outlined above. As we mentioned, in this
case, only Condition (\ref{eq:thm5}) needs to be proved.
There are two cases. If $F$ is different from $F_1$, then
the Clark
completion of $F$ in
both $P_1$ and $P_2$ is the same. Suppose it is
$(\exists s)F(s)\equiv \Phi_F$.
By Corollary~\ref{closedform}, we have
\[
{\cal D}_2\models (\forall s). F(s)\supset
(\exists s')(s'<s\land \Phi_F'(s)),
\]
where ${\cal D}_2$ is the action theory of $P_2$, and $\Phi_F'$ is the result
of replacing in $\Phi_F$ every positive subformula of the form 
$(\exists s)F'(\vec{t},s)$ by $F'(\vec{t},s)$. Now by the 
construction of $\Psi_F$, we have
\[
{\cal D}_2\cup {\cal F}\models (\forall s). F(s)\supset
(\exists s')(s'<s\land \Psi_F(s)),
\]
which is the condition (\ref{eq:thm5}).

For $F_1$, we need to check:
\begin{equation}
\label{proof11}
{\cal D}_2\cup {\cal F}\models (\forall s). F_1(s)\supset
(\exists s')(s'<s\land \Psi_{F_1}(s)).
\end{equation}

Using Corollary~\ref{closedform} for $P_2$, 
and the Clark completion (\ref{proof10})
of $F_1$ in $P_2$, we have
\begin{equation}
\label{proof12}
{\cal D}_2\cup {\cal F}
\models 
(\forall s).  F_1(s)\supset (\exists s')\{ s'< s\land 
[(F_1(s')\land G[s'])\lor
\Psi_{F_1}(s')]\}.
\end{equation}
Now assume that ${\cal D}_2\cup {\cal F}$, and
$F_1(s)$. Since $\neg F_1(S_0)$, by our foundational axioms for the
situation calculus, there is a situation of the form $do(a,s')\leq s$ such that
\[
F_1(do(a,s'))\land (\forall s^*)(s^*\leq s'\supset \neg F_1(s^*)).
\]
By (\ref{proof12}), this means that $\Psi_{F_1}(s')$ must hold.
So we have (\ref{proof11}).
\end{proof}

\subsection{Unfold/Fold}

Unfold/fold (Tamaki and Sato \cite{TamakiSato84}) are among 
the best known program transformation operators.
Seki \cite{Seki93} shows that they preserve the well-founded semantics of
(Van Gelder and Ross and Schlipf \cite{VanGelder88}).
Using Theorem~\ref{th:equivalence}, we can show, rather straightforwardly,
that
unfold/fold also preserve our situation calculus semantics. We illustrate using
unfolding. For ease of presentation, we consider only the propositional case.
The following definition is adapted from (Seki \cite{Seki93}).

Let $P$ be a logic program, and $C$ a clause in $P$ of the form:
\begin{lprule}
$F_1$ :- $F_2$ \& $G$
\end{lprule}
where $F_1$ and $F_2$ are distinct atoms.
Suppose that
\begin{lprule}
$F_2$ :- $G_1$\\
\hspace{2em}\vdots\\
$F_2$ :- $G_k$
\end{lprule}
are all of the clauses in the definition of $F_2$ in $P$.
Let $C_i$, $1\leq i\leq k$, be the result of replacing $F_2$ in $C$
by $G_i$. Then the program $P'=(P-\{ C\})\cup \{ C_1,...,C_k\}$ is called
an {\em unfolding} of $P$. The clause $C$ is called the {\em unfolding clause}.

\begin{proposition}
If $P'$ is an unfolding of $P$, then $P$ and $P'$ are equivalent.
\end{proposition}
\begin{proof}
Suppose that the Clark completion of $F_1$ in $P$ is of the form
\begin{equation}
\label{proof1}
(\exists s)F_1(s)\equiv [((\exists s)F_2(s)\land \var])\lor \Phi].
\end{equation}
Then the Clark completion of $F_1$ in $P'$ is of the form
\begin{equation}
(\exists s)F_1(s)\equiv [(\var_1\land \var)\lor
\cdots\lor\nonumber  (\var_k\land \var)\lor
 \Phi]. \label{proof2}
\end{equation}
The Clark completion of $F_2$ in both programs is of the form
\begin{equation}
\label{proof3}
(\exists s)F_2(s)\equiv [\var_1\lor\cdots\lor \var_k].
\end{equation}
Notice that (\ref{proof2}) is a consequence of (\ref{proof1}) and
(\ref{proof3}).

We show that the answer theory of $P$ entails that of $P'$.\\[1ex]
{\bf Condition }(\ref{eq:thm3}). We only need to show this for the new clauses
$C_i$, $1\leq i\leq k$ in $P'$:
\[
{\cal D}\models (\exists s)(G_i[s]\land G[s])\supset
 (\exists s)F_1(s).
\]
But $(\exists s)(G_i[s]\land G[s])$ is equivalent to
$\var_i\land \var$
(see Proposition~\ref{proposition2} and Theorem~\ref{clarkcompletion}).
So this follows from (\ref{proof1}) and (\ref{proof3}).\\[1ex]
{\bf Conditions} (\ref{eq:thm4}) and (\ref{eq:thm5}). We only need to show these
two conditions for $F_1$, since the Clark completion for other fluents are
the same for both programs (see the above
proof of Proposition~\ref{simpleequiv}).
We take $\Psi_{F_1}(s)$ to be the formula obtained
from the Clark completion (\ref{proof2}) for $F_1$ in $P'$ as outlined
following Theorem~\ref{th:equivalence}.
We only need to prove (\ref{eq:thm5}):
\[
{\cal D}\cup {\cal F}\models (\forall s). F_1(s)\supset 
 (\exists s')(s'< s\land \Psi_{F_1}(s')).
\]
Assume that ${\cal D}\cup {\cal F}$ and $F_1(s)$. 
By
Corollary~\ref{closedform}, and the Clark completion (\ref{proof1})
for $F_1$ in $P$, there is a $s'\leq s$ such that
\[
(F_2(s')\land G[s'])\lor \Phi'(s'),
\]
where $\Phi'(s)$ is the result of dropping $(\exists s)$ from all the
positive occurrence of the subformula $(\exists s)F(s)$ in $\Phi$.
>From $F_2(s')$, by Corollary~\ref{closedform} for $F_2$, 
there is a $s^* < s'$ such that
\[
\{ (G_1[s^*]\lor\cdots\lor G_k[s^*])\land G[s']\}\lor \Phi'(s').
\]
Now by Corollary~\ref{corollary1}, we have
\[
\{ (G_1[s']\lor\cdots\lor G_k[s'])\land G[s']\}\lor \Phi'(s').
\]
By the definition of $\Psi_{F_1}(s)$, the above formula is equivalent
to $\Psi_{F_1}(s')$ under the assumption that ${\cal F}$.
This proves the condition (\ref{eq:thm5}), thus the answer theory of $P$
entails that of $P'$.

The converse has a much easier proof, with the same formula $\Psi_{F_1}(s)$
for conditions (\ref{eq:thm4}) and (\ref{eq:thm5}).
We do it for condition (\ref{eq:thm5}), because this is the
only nontrivial one. We need to show
\[
{\cal D}'\cup {\cal F}\models (\forall s). F_1(s)\supset 
 (\exists s')(s'< s\land \Psi_{F_1}(s')).
\]
Assume that ${\cal D}'\cup {\cal F}$ and $F_1(s)$. By
Corollary~\ref{closedform} for $F_1$ in $P'$,
there is a $s'\leq s$ such that
\[
(G_1[s']\land G[s'])\lor \cdots\lor
(G_k[s']\land G[s'])\lor \Phi'(s').
\]
Again by the definition of $\Psi_{F_1}(s)$, the above formula is equivalent
to $\Psi_{F_1}(s')$ under the assumption that ${\cal F}$.
This proves condition (\ref{eq:thm5}).
\end{proof}

This proof generalizes to the first order case; we omit the details.




\section{Other Applications}
\label{other}
The framework of this paper is very
general; it can be used to formalize many other aspects of logic
programming languages. 

Like most work on the formal semantics of logic programs, we have ignored many
``dirty aspects'' of the language, such as the cut operator.
As mentioned earlier, one of the advantages of treating rules as
actions is that we can reason about
them as first-order objects within the logic. This is particularly useful in
formalizing many search control operators in logic programming.
As an example, we have formalized the cut ($\cut$) operator in Prolog
using the basic framework proposed here (\cite{Lin:cut}). 

Briefly,
given a definite
logic program $P$ that contains cut, we proceed as follows
to provide a semantics for $P$. First, we ignore cut, and delete all
occurrences of $\cut$ in $P$. This will give us a
program that does not mention $\cut$, so the theory of this paper will
be applicable, and an
action theory $\cal D$ for it can be constructed.
As we emphasized before, in $\cal D$, situations
are derivation histories. However, due to
the presence of $\cut$, some situations may not be reachable.
A logical characterization of cut is then achieved by adding to
$\cal D$ a situation calculus sentence that axiomatizes the set of
reachable situations.
We show that this semantics is well-behaved when
the logic program is properly stratified. Furthermore, according to
this semantics, the usual implementation of the negation-as-failure
operator using cut is provably correct with respect to the stable model
semantics. For details see \cite{Lin:cut}.

We are also currently exploring the possibility of formalizing the dynamic
``assert'' and ``retract'' operators of Prolog within this framework.
It is particularly interesting that once we allow ``retract'', the resulting
theories of actions become much richer in that some actions will now
have negative effects on fluents, and issues such as goal interactions
in planning become relevant.

\section{Concluding Remarks}

By taking seriously the idea that rules are actions, we 
have formalized the declarative meaning of logic programs in the
situation calculus. Like Clark's completion, our situation calculus
semantics is formulated in classical logic. Unlike Clark's completion,
our semantics is strong enough to handle recursion. Having a classical
logical semantics 
has many advantages, one of which is the relative ease of
proving properties of programs. To illustrate this,
we have formulated conditions for two logic
programs to be equivalent, and used them to prove the correctness of the
unfolding transformation of (Tamaki and Sato \cite{TamakiSato84}).

We have also used this framework to formalize various search control operators,
and are working on extending it to the dynamic ``assert'' and ``retract''
operators of Prolog.


\section*{Acknowledgements}

Our thanks to the other members of the University of Toronto
Cognitive Robotics Group (Yves Lesp\'erance,
Hector Levesque, and Daniel Marcu) for their ideas,
suggestions, and comments.
Thanks also to G. Neelakantan Kartha,
and Vladimir Lifschitz
for helpful comments on an earlier draft of this paper. Our special
thanks to Vladimir for bringing to our attention the work of
Wallace \cite{Wallace93}. 
This research was supported by grants from the National Science
and Engineering Research Council of Canada, the Institute for
Robotics and Intelligent Systems of
Canada, and the Information Technology Research Center of Ontario.


\begin{thebibliography}{10}

\bibitem{Clark78}
K.~L. Clark.
\newblock Negation as failure.
\newblock In H.~Gallaire and J.~Minker, editors, {\em Logics and Databases},
  pages 293--322. Plenum Press, New York, 1978.

\bibitem{Fitting85}
M.~Fitting.
\newblock A {K}ripke-{K}leene semantics for logic programs.
\newblock {\em Journal of Logic Programming}, 2(4):295--312, 1985.

\bibitem{GelfondLifschitz88}
M.~Gelfond and V.~Lifschitz.
\newblock The stable model semantics for logic programming.
\newblock In {\em Proc. Fifth International Conference and Symposium on Logic
  Programming}, pages 1070--1080, 1988.

\bibitem{Green69}
C.~C. Green.
\newblock Application of theorem proving to problem solving.
\newblock In {\em Proceedings of the International Joint Conference on
  Artificial Intelligence (IJCAI--69)}, pages 219--239, 1969.

\bibitem{Haas87}
A.~R. Haas.
\newblock The case for domain-specific frame axioms.
\newblock In F.~M. Brown, editor, {\em The Frame Problem in Artificial
  Intelligence. Proceedings of the 1987 Workshop on Reasoning about Action},
  pages 343--348, San Jose, CA, 1987. Morgan Kaufmann Publishers, Inc.

\bibitem{Kunen87}
K.~Kunen.
\newblock Negation in logic programming.
\newblock {\em Journal of Logic Programming}, 4(4):289--308, 1987.

\bibitem{levesquereiter:golog}
H.J.~Levesque, R.~Reiter, Y.~Lesp\'{e}rance, F.~Lin and
R. Scherl. 
\newblock GOLOG: A logic programming language for dynamic domains.
\newblock {\em Journal of Logic Programming}, this volume.

\bibitem{Lifschitz:pointwise}
V.~Lifschitz.
\newblock Pointwise circumscription.
\newblock In {\em Proceedings of the Fifth National Conference on Artificial
  Intelligence (AAAI--86)}, pages 406--410, Philadelphia, PA, 1986.

\bibitem{Lifschitz:action}
V.~Lifschitz.
\newblock Formal theories of action.
\newblock In {\em Proceedings of the Tenth International Joint Conference on
  Artificial Intelligence (IJCAI--87)}, pages 966--972, 1987.

\bibitem{Lin:cut}
F.~Lin.
\newblock A situation calculus semantics for the prolog cut operator.
\newblock http://www.cs.toronto.edu/\~\ \hspace{-2.6mm} cogrobo/, Draft. 1995.

\bibitem{LinReiter:constraint}
F.~Lin and R.~Reiter.
\newblock State constraints revisited.
\newblock {\em Journal of Logic and Computation, Special {I}ssue on {A}ctions
  and {P}rocesses}, 4(5):655--678, 1994.

\bibitem{LinReiter:forgetting}
F.~Lin and R.~Reiter.
\newblock Forget it!
\newblock In R.~Greiner and D.~Subramanian, editors, {\em Working Notes of AAAI
  Fall Symposium on Relevance}, pages 154--159. The American Association for
  Artificial Intelligence, Menlo Park, CA, November 1994.

\bibitem{LinShoham95}
F.~Lin and Y.~Shoham.
\newblock Provably correct theories of action.
\newblock {\em Journal of the ACM}, 42(2):293--320, 1995.

\bibitem{Lloyd87}
J.~W. Lloyd.
\newblock {\em Foundations of Logic Programming}.
\newblock Springer-Verlag, 2nd edition, 1987.

\bibitem{mccarthy63}
J.~McCarthy.
\newblock Situations, actions and causal laws.
\newblock In M.~Minsky, editor, {\em Semantic Information Processing}, pages
  410--417. MIT Press, Cambridge, Mass., 1968.

\bibitem{McCarthy86}
J.~McCarthy.
\newblock Applications of circumscription to formalizing commonsense knowledge.
\newblock {\em Artificial Intelligence}, 28:89--118, 1986.

\bibitem{McCarthyHayes69}
J.~McCarthy and P.~Hayes.
\newblock Some philosophical problems from the standpoint of artificial
  intelligence.
\newblock In B.~Meltzer and D.~Michie, editors, {\em Machine Intelligence 4},
  pages 463--502. Edinburgh University Press, Edinburgh, 1969.

\bibitem{Pednault88}
E.~P. Pednault.
\newblock Synthesizing plans that contain actions with context-dependent
  effects.
\newblock {\em Computational Intelligence}, 4:356--372, 1988.

\bibitem{pednault89}
E.~P. Pednault.
\newblock {ADL}: Exploring the middle ground between {STRIPS} and the situation
  calculus.
\newblock In {\em Proceedings of the First International Conference on
  Principles of Knowledge Representation and Reasoning (KR'89)}, pages
  324--332. Morgan Kaufmann Publishers, Inc., 1989.

\bibitem{Przymusinski88}
T.~C. Przymusinski.
\newblock On the declarative semantics of deductive databases and logic
  programs.
\newblock In J.~Minker, editor, {\em Foundations of Deductive Databases and
  Logic Programming}, pages 193--216. Morgan Kaufmann, Los Altos, CA, 1988.

\bibitem{Reiter91}
R.~Reiter.
\newblock The frame problem in the situation calculus: a simple solution
  (sometimes) and a completeness result for goal regression.
\newblock In V.~Lifschitz, editor, {\em Artificial Intelligence and
  Mathematical Theory of Computation: Papers in Honor of John McCarthy}, pages
  418--420. Academic Press, San Diego, CA, 1991.

\bibitem{Reiter:<}
R.~Reiter.
\newblock Proving properties of states in the situation calculus.
\newblock {\em Artificial Intelligence}, 64:337--351, 1993.

\bibitem{Sagiv88}
Y.~Sagiv.
\newblock Optimizing datalog programs.
\newblock In J.~Minker, editor, {\em Foundations of Deductive Databases and
  Logic Programming}, pages 659--698. Morgan Kaufmann Publishers, San Mateo,
  CA., 1988.

\bibitem{Schubert90}
L.~K. Schubert.
\newblock Monotonic solution to the frame problem in the situation calculus: an
  efficient method for worlds with fully specified actions.
\newblock In H.~Kyberg, R.~Loui, and G.~Carlson, editors, {\em Knowledge
  Representation and Defeasible Reasoning}, pages 23--67. Kluwer Academic
  Press, Boston, MA, 1990.

\bibitem{Seki93}
H.~Seki.
\newblock Unfold/fold transformation of general logic programs for the
  well-founded semantics.
\newblock {\em The Journal of Logic Programming}, 15:5--23, 1993.

\bibitem{Shoham88}
Y.~Shoham.
\newblock Chronological ignorance: experiments in nonmonotonic temporal
  reasoning.
\newblock {\em Artificial Intelligence}, 36:279--331, 1988.

\bibitem{TamakiSato84}
H.~Tamaki and T.~Sato.
\newblock Unfold/fold transformation of logic programs.
\newblock In {\em Proceedings of the 2nd International Conference on Logic
  Programming}, pages 127--138, 1984.

\bibitem{vanGelder89}
A.~{Van Gelder}.
\newblock Negation as failure using tight derivations for general logic
  programs.
\newblock {\em Journal of Logic Programming}, 6(2):109--133, 1989.

\bibitem{VanGelder88}
A.~{Van Gelder}, K.~A. Ross, and J.~S. Schlipf.
\newblock Unfounded sets and well-founded semantics for general logic programs.
\newblock In {\em Proc. Seventh ACM Symposium on Principles of Database
  Systems}, pages 221--230, 1988.

\bibitem{Waldinger77}
R.~Waldinger.
\newblock Achieving several goals simultaneously.
\newblock In E.~Elcock and D.~Michie, editors, {\em Machine Intelligence},
  pages 94--136. Ellis Horwood, Edinburgh, Scotland, 1977.

\bibitem{Wallace93}
M.~G. Wallace.
\newblock Tight, consistent, and computable completions for unrestricted logic
  programs.
\newblock {\em Journal of Logic Programming}, 15:243--273, 1993.

\end{thebibliography}



\end{document}
------- End of forwarded message -------

