% 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~~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'~~~~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 -------
~~