%15-40 pages
%logical notations: Circumscription, by Lifschitz
\documentclass[fleqn,10pt]{memoir}
\usepackage{latexsym}
\usepackage{FAI}
\usepackage{amsfonts}
\usepackage{amssymb}
\newcommand{\myalign}{&\hspace{-.2in}&}
\long\def\comment#1{}
\newcommand{\D}{\:\: |\:\:}
\newtheorem{theorem}{Theorem}
\begin{document}
\bibliographystyle{abbrv}
\chaptertitleauthors{Situation Calculus}{Fangzhen Lin}
\authormark{Fangzhen Lin}

The situation calculus \index{the situation calculus}is a logical language for representing
changes. It was first introduced by McCarthy in 1963,\footnote{In a
Stanford Technical Report that was later published as
\cite{McCarthy63}.} and described in further details by McCarthy and
Hayes \cite{McCarthyHayes69} in 1969.

The basic concepts in the situation calculus are
\emph{ situations}\index{situation}, \emph{ actions} \index{action} and \emph{ fluents}\index{fluent}.
Briefly,
actions are what make the dynamic world change from one situation to another
when performed by agents. 
Fluents are situation-dependent functions used to describe 
the effects of actions. There are two kinds of them,
\emph{relational} fluents \index{relational fluent} and \emph{functional} fluents\index{functional fluent}. 
The former have only two values: true or false, while the latter can take
a range of values.
For instance, one may have a relational fluent called $handempty$ which
is true in a situation if the robot's hand is not holding anything.
We may need a relation like this in a robot domain.
One may also have a 
functional fluent called $battery\mbox{-}level$ whose value in a situation is an integer
between 0 and 100 denoting the total battery power remaining
on one's laptop computer.

%The meaning of situations varies depending on the authors.
According to McCarthy and Hayes \cite{McCarthyHayes69},
a situation is
``the complete state of the universe at an instance of time.''  
But for Reiter \cite{Reiter:book}, 
a situation is the same as its history which is the finite 
sequence of actions that has been performed since the initial situation $S_0$. 
We shall discuss Reiter's foundational axioms that make this precise later.
Whatever the interpretation, the unique feature of the situation calculus is
that situations are first-order objects that can be quantified over. This
is what makes the situation calculus a powerful formalism for representing
change, and distinguishes it from other formalisms such as dynamic
logic \cite{Harel79}.


To describe a dynamic domain in the situation calculus, one has to decide
on the set of actions available for the agents to perform, and the set of fluents
needed to describe the changes these actions will have on the world.
For example, 
consider the classic blocks world \index{the blocks world} where some blocks of equal size can be
arranged into a set of towers on a table. The set of actions in this domain
depends on what the imaginary agent can do. If we imagine the agent to be
a one-handed robot that can be directed to grasp any block that is on the top
 of
a tower, and either add it to the top of another tower or put it down 
on the table to make a new tower,
then we can have the following actions
\cite{Nilsson80}:
\begin{itemize}
\item $stack(x,y)$ - put block $x$ on block $y$, provided the robot is holding
$x$, and $y$ is clear, i.e. there is no other block on it;
\item $unstack(x,y)$ - pick up block $x$ from block $y$, provided the robot's hand is empty,
$x$ is on $y$, and $x$ is clear;
\item $putdown(x)$ - put block $x$ down on the table, provided the robot is 
holding $x$;
\item $pickup(x)$ - pick up block $x$ from the table, 
provided the robot's hand is empty,
$x$ is on the table and clear.
\end{itemize}
To describe the effects of these actions, we can use the following 
relational fluents:
\begin{itemize}
\item $handempty$ - true in a situation if the robot's hand is empty; 
\item $holding(x)$ - true in a situation if the robot's hand is holding
block $x$;
\item $on(x,y)$ - true in a situation if block $x$ is on block $y$;
\item $ontable(x)$ - true in a situation if block $x$ is on the table;
\item $clear(x)$ - true in a situation if block $x$ is the top block of
a tower, i.e. the robot is not holding it, and there is no other block on
it.
\end{itemize}
So for example, we can say that for action $stack(x,y)$ to be performed in
a situation, $holding(x)$ and $clear(y)$ must be true, and that after
$stack(x,y)$ is performed, in the resulting
new situation, $on(x,y)$ and $handempty$
will be true, and $holding(x)$ and $clear(y)$ will no longer be true.

If, however, the agent in this world can move a block from
a clear position to another clear position, then we only need the following
action:
\begin{itemize}
\item $move(x,y)$ - move block $x$ to position $y$,
provided that block $x$ is clear to move, where a position
is either a block or the table.
\end{itemize}
To describe the effects of this action, it suffices to use two fluents
$on(x,y)$ and $clear(x)$: action $move(x,y)$ can be performed in
a situation if $x\neq table$, $clear(x)$, and $clear(y)$ are true in the
situation, and that after $move(x,y)$ is performed, in the resulting new
situation, $x$ is no longer where it was but on $y$ now.

To axiomatize dynamic domains like these in the situation calculus, we will need to be a bit
more precise about the language.

\section{Axiomatizations}

We said that the situation calculus \index{the situation calculus} 
is a logical language for reasoning
about change. More precisely, it is a first-order language, sometime
enriched with some second-order features. It represents situations and
actions as first-order objects that can be quantified over. Thus we can 
have a first-order sentence saying that among all actions, $putdown(x)$
is the only one that can make $ontable(x)$ true. We can also have a first-order
sentence saying that in any situation, executing different actions will
always yield different situations. 
As we mentioned, being able to quantify over situations makes the situation calculus a very expressive language,
and distinguishes it
from other formalisms for representing dynamic systems.

As we mentioned, fluents are functions on situations. Of special interest
are relational fluents that are either true or false in a situation.
Initially, McCarthy and Hayes
represented relational
fluents as predicates whose last argument is a situation term
\cite{McCarthyHayes69}. For instance, to say that block $x$ is on the table
in situation $s$, one would use a binary predicate like $ontable$ and write
$ontable(x,s)$.
This was also the approach taken
by Reiter \cite{Reiter91,Reiter:book}. Later, McCarthy \cite{McCarthy77,McCarthy02}
proposed to reify relational
fluents as first-order objects as well, and introduced a special binary
predicate ``$Holds(p,s)$'' to express the truth value of a relational
fluent $p$
in situation $s$. Here we shall follow McCarthy's later work, and represent
relational fluents as first-order objects as well. This allows us
to quantify over fluents. But more importantly, it allows us to talk about
other properties of fluents like causal relationships among them 
\cite{Lin:causality}. One could continue to write formulas like 
$ontable(x,s)$, which will be taken as a shorthand for $Holds(ontable(x),s)$.

To summarize, the situation calculus is a first-order language with the 
following special sorts: \emph{situation}, \emph{action}, and 
\emph{fluent} (for relational fluents). There could be other sorts, some of them
domain dependent like
\emph{block} for blocks in the blocks world or \emph{loc} for locations in
logistics domain, and others domain independent like \emph{truth} for truth
values.  For now we assume
the following special domain independent predicates and functions:
\begin{itemize}
\item $Holds(p,s)$ - fluent $p$ is true in situation $s$;
\item $do(a,s)$ - the situation that results from performing action $a$ in situation
$s$;
\item $Poss(a,s)$ - action $a$ is executable in situation $s$.
\end{itemize}
Other special predicates and functions may be introduced. For instance,
to specify Golog programs \cite{golog}, one can use 
a ternary predicate called $Do(P,s_1,s_2)$, meaning
that $s_2$ is a terminating situation of performing program $P$ in $s_1$.
To specify causal relations among fluents, one can use another ternary predicate
$Caused(p,v,s)$, meaning that fluent $p$ is caused to have truth value $v$
in situation $s$.

Under these conventions, a relational fluent is represented by a function
that does not have a situation argument, and a functional fluent is
represented by a function whose last argument is of sort $situation$.
For instance, $clear(x)$ is a unary relational fluent. We often write
$clear(x,s)$ which as we mentioned earlier, is just a shorthand for 
$Holds(clear(x),s)$.
On the other hand, $color(x,s)$ is a binary functional fluent, and we write
axioms about it like
\[
color(x,do(paint(x,c),s)) = c.
\]

We can now axiomatize our first blocks world domain with the following
first-order sentences (all free variables are assumed to be universally
quantified):
\begin{eqnarray}
\label{eq:blocks-world10}
\myalign
Poss(stack(x,y),s)\equiv holding(x,s)\land clear(y,s),\\
\myalign
Poss(unstack(x,y),s)\equiv on(x,y,s)\land clear(x,s)\land handempty(s),\\
\myalign
Poss(pickup(x),s)\equiv ontable(x,s)\land clear(x,s)\land handempty(s),\\
\myalign
Poss(putdown(x),s)\equiv holding(x,s),\\
\myalign
holding(u,do(stack(x,y),s))\equiv 
holding(u,s)\land u\neq x, \label{stack1}\\
\myalign
handempty(do(stack(x,y),s)),\\
\myalign
on(u,v,do(stack(x,y),s))\equiv
 (u=x\land v=y)\lor on(u,v,s),\\
\myalign
clear(u,do(stack(x,y),s))\equiv 
 u=x\lor (clear(u,s)\land u\neq y),\\
\myalign
ontable(u,do(stack(x,y),s))\equiv
ontable(u,s),\label{stack5}\\
\myalign
holding(u,do(unstack(x,y),s))\equiv u=x,\\
\myalign
\neg handempty(do(unstack(x,y),s)),\\
\myalign
on(u,v,do(unstack(x,y),s))\equiv 
 on(u,v,s)\land \neg (x=u\land y=v),\\
\myalign
clear(u,do(unstack(x,y),s))\equiv 
 u=y\lor (clear(u,s)\land u\neq x),\\
\myalign
ontable(u,do(unstack(x,y),s))\equiv 
ontable(u,s),\\
\myalign
holding(u,do(pickup(x),s))\equiv u=x,\\
\myalign
\neg handempty(do(pickup(x),s)),\\
\myalign
on(u,v,do(pickup(x),s))\equiv
 on(u,v,s),\\
\myalign
clear(u,do(pickup(x),s))\equiv 
 clear(u,s)\land u\neq x,\\
\myalign
ontable(u,do(pickup(x),s))\equiv 
ontable(u,s)\land x\neq u,\\
\myalign
holding(u,do(putdown(x),s))\equiv holding(u,s)\land u\neq x,\\
\myalign
handempty(do(putdown(x),s)),\\
\myalign
on(u,v,do(putdown(x),s))\equiv
on(u,v,s),\\
\myalign
clear(u,do(putdown(x),s))\equiv
 u=x\lor clear(u,s),\\
\myalign
ontable(u,do(putdown(x),s))\equiv 
u=x\lor ontable(u,s).
\label{eq:blocks-world11}
\end{eqnarray}
Similarly, we can write the following axioms for our second version of
the blocks world
domain.
\begin{eqnarray}
\label{eq:blocks-world20}
\myalign
Poss(move(x,y),s)\equiv x\neq table\land clear(x,s)\land clear(y,s)
\\
\myalign
clear(u,do(move(x,y),s))\equiv \nonumber\\
\myalign\hspace{5em} 
u=table\lor on(x,u,s)\lor (clear(u,s)\land u\neq y),\\
\myalign
on(u,v,do(move(x,y),s))\equiv \nonumber\\
\myalign\hspace{5em} 
(x=u\land y=v)\lor
  (on(u,v,s)\land u\neq x)
\label{eq:blocks-world21}
\end{eqnarray}

\section{The frame, the ramification and the qualification problems}

The set of axioms (\ref{eq:blocks-world10}) - (\ref{eq:blocks-world11})
provides a complete logical characterization of the effects of actions
for our first blocks world domain. For each action, it gives necessary and
sufficient conditions for it to be executable in any situation, and 
fully specifies the effects of this action on every fluent.
Similarly, the set of axioms
(\ref{eq:blocks-world20}) - (\ref{eq:blocks-world21}) completely captures
the effects of actions for our second blocks world domain.

However, there is something unsatisfying about these two sets of axioms.
When we informally described the effects of actions, we did not describe
it this way. For instance, we said that
after $stack(x,y)$ is performed, in the resulting
new situation, $on(x,y)$ and $handempty$
will be true, and $holding(x)$ and $clear(y)$ will no longer be true. We did
not have to say, for instance, that if $y$ is initially on the table, it will
still be on the table. Many researchers believe that when people remember
the effects of an action, they do not explicitly store
the facts that are not changed by the action, rather they just remember the
changes that this action will bring about. Consequently, when we axiomatize
an action, we should only need to specify the changes that will be made by the
action. But if
we specify in our theory
only the changes that an action will make, there is then a problem of
how to derive those that are not changed by the action. This problem
was identified by McCarthy and Hayes \cite{McCarthyHayes69} in 1969,
and they called it \index{the frame problem} \emph{the frame problem}.
For our blocks world example, we can view the frame problem as the
problem of looking for an appropriate logic that when given, for
example the following so-called ``effect axioms'' about $stack(x,y)$:
\begin{eqnarray*}
\myalign
on(x,y,do(stack(x,y),s)),\\
\myalign
clear(x,do(stack(x,y),s)),\\
\myalign
\neg clear(y,do(stack(x,y),s)),\\
\myalign
handempty(do(stack(x,y),s)),\\
\myalign
\neg holding(x,do(stack(x,y),s)),
\end{eqnarray*}
will derive a complete specification of the effects of action $stack(x,y)$,
like what the set of axioms (\ref{stack1}) - (\ref{stack5})
does  in first-order logic \cite{LinShoham95}.

The frame problem is one of the most
well-known
AI problems, if not the most well-known one, and a lot of work has been done on
solving it. It motivated much of the early work on nonmonotonic
logic (see papers in \cite{Ginsberg87} and Chapter 6). 
While the problem 
was identified in the situation calculus, it shows up in other formalisms
like the event calculus (Chapter 17), temporal action logics (Chapter 18),
and nonmonotonic causal logic (Chapter 19). In fact, the general consensus
is that any formalism for reasoning about change will have to deal with it.

McCarthy \cite{McCarthy86} initially 
proposed to solve the frame problem by the 
following generic \index{frame axioms} frame axiom:
\begin{equation}
\label{abnormal}
Holds(p,s)\land \neg abnormal(p,a,s)\supset Holds(p,do(a,s))
\end{equation}
with the abnormality predicate $abnormal$ circumscribed. 
Hanks and McDermott
\cite{HanksMcDermott87} showed that this approach,
unfortunately, does not produce the
intended result on
the \index{Yale Shooting Problem} Yale Shooting Problem (YSP). This is a
simple problem with three actions: $wait$ (do nothing),
$load$ (load the gun), and $shoot$ (fire the gun). Their effects can be
axiomatized by the following axioms:
\begin{eqnarray}
\myalign
loaded(do(load,s)), \label{ysp1}\\
\myalign
loaded(s)\supset dead(do(shoot,s)). \label{ysp2}
\end{eqnarray}
Now suppose $S_0$ is a situation where the gun is not loaded and Fred is alive:
\begin{equation}
\label{ysp3}
\neg loaded(S_0)\land \neg dead(S_0).
\end{equation}
Hanks and McDermott showed that the circumscription of $abnormal$ in
the theory 
$$\{ (\ref{abnormal}),(\ref{ysp1}),(\ref{ysp2}),(\ref{ysp3})\}$$
with $Holds$ allowed to vary has two models, one in which 
\begin{eqnarray*}
\myalign
loaded(do(load,S_0)),\\
\myalign
loaded(do(wait,do(load,S_0))),\\
\myalign
dead(do(shoot,do(wait,do(load,S_0))))
\end{eqnarray*}
are true as desired, and the other in which
\begin{eqnarray*}
\myalign
loaded(do(load,S_0)),\\
\myalign \neg loaded(do(wait,do(load,S_0))),\\
\myalign
\neg dead(do(shoot,do(wait,do(load,S_0))))
\end{eqnarray*}
are true, which are counter-intuitive as the action $wait$, which is
supposed to do nothing, mysteriosly unloaded the gun.

For the next few years, the YSP motivated much of the work on the frame
problem, and the frame problem became the focus
of the research on nonmonotonic reasoning. In response to the problem,
Shoham \cite{Shoham88} proposed \index{chronological minimization} chronological minimization that prefers
changes at later times. 
%Lifschitz proposed a new version of circumscription
%called pointwise circumscription \cite{Lifschitz:pointwise} that can 
%be used to capture this new notion of minimization.
Many other proposals were put forward (e.g. 
\cite{Lifschitz:pointwise,Lifschitz:action, Baker91, Reiter91, LinShoham95, Sandewall:book, Lin:causality, Thielscher97,McCainTurner97}). 

The thrust of modern solutions to the frame problem is to separate the
specification of the effects of actions from the tasks of reasoning about these
actions. For instance, given the effect axioms (\ref{ysp1}) and (\ref{ysp2}),
one can obtain the following complete specification of the effects of
the actions concerned:
\begin{eqnarray*}
\myalign
loaded(do(load,s)),\\
\myalign
dead(do(load,s))\equiv dead(s),\\
\myalign
loaded(do(shoot,s))\equiv loaded(s),\\
\myalign
dead(do(shoot,s))\equiv loaded(s)\lor dead(s),\\
\myalign
loaded(do(wait,s))\equiv loaded(s),\\
\myalign
dead(do(wait,s))\equiv dead(s).
\end{eqnarray*}
Now given the initial state axiom (\ref{ysp3}), one can easily infer that
$dead(do(shoot,do(wait,do(load,S_0))))$ holds.

This separation between the specification of action theories and the tasks
of reasoning under these theories can be done syntactically by
distinguishing general effect axioms like (\ref{ysp1}) from specific facts
like (\ref{ysp3}) about some particular situations, as in Reiter's solution
\cite{Reiter91}
that we shall describe next. It can also be done by encoding general effect
axioms in a special language using predicates like $Caused$, as in Lin's
causal theories of action 
\cite{Lin:causality} for solving the ramification problem.

\subsection{The frame problem - Reiter's solution}

Based on earlier work by Pednault \cite{Pednault89}, Haas \cite{Haas87}
and Schubert \cite{Schubert90}, Reiter \cite{Reiter91,Reiter:book} proposed a simple
syntactic manipulation much in the style of Clark's predicate completion
\cite{Clark78} (see Chapter 7) that turns a set of effect axioms into a set of successor
state axioms that completely captures the true value of each fluent in any
successor situation.
%, thus solves the frame problem. 
It is best to illustrate
Reiter's method by an example. Consider our first blocks world domain, and
let us write down all the effect axioms:
\begin{eqnarray}
\label{eqn:blocks1-effect1}
\myalign
on(x,y,do(stack(x,y),s)),\\
\myalign
clear(x,do(stack(x,y),s)),\\
\label{eqn:blocks1-effect2}
\myalign
\neg clear(y,do(stack(x,y),s)),\\
\myalign
handempty(do(stack(x,y),s)),\\
\myalign
\neg holding(x,do(stack(x,y),s)),\\
\myalign
\neg on(x,y,do(unstack(x,y),s)),\\
\myalign
\neg clear(x,do(unstack(x,y),s)),\\
\myalign
clear(y,do(unstack(x,y),s)),\\
\myalign
\neg handempty(do(unstack(x,y),s)),\\
\myalign
holding(x,do(unstack(x,y),s)),\\
\myalign
ontable(x,do(putdown(x),s)),\\
\myalign
clear(x,do(putdown(x),s)),\\
\myalign
handempty(do(putdown(x),s)),\\
\myalign
\neg holding(x,do(putdown(x),s)),\\
\myalign
\neg ontable(x,do(pickup(x),s)),\\
\myalign
\neg clear(x,do(pickup(x),s)),\\
\myalign
\neg handempty(do(pickup(x),s)),\\
\myalign
holding(x,do(pickup(x),s)).
\end{eqnarray}
Now for each of these effect axioms, transform it into one of the following two forms:
\begin{eqnarray*}
\myalign
\gamma(a,\vec{x},s)\supset F(\vec{x},do(a,s)),\\
\myalign
\gamma(a,\vec{x},s)\supset \neg F(\vec{x},do(a,s)).
\end{eqnarray*}
For instance, the effect axiom (\ref{eqn:blocks1-effect1}) can be transformed
equivalently into the following axiom:
\[
a=stack(x,y)\supset on(x,y,do(a,s)),
\]
and the effect axiom (\ref{eqn:blocks1-effect2}) can be transformed
equivalently into the following axiom:
\[
(\exists y)a=stack(y,x)\supset \neg clear(x,do(a,s)).
\]
Now for each fluent $F$, suppose the following is the list of
all such axioms so obtained:
\begin{eqnarray*}
\myalign
\gamma^+_1(a,\vec{x},s)\supset F(\vec{x},do(a,s)),\\
\myalign\cdots\\
\myalign
\gamma^+_m(a,\vec{x},s)\supset F(\vec{x},do(a,s)),\\
\myalign
\gamma^-_1(a,\vec{x},s)\supset \neg F(\vec{x},do(a,s)),\\
\myalign\cdots\\
\myalign
\gamma^-_n(a,\vec{x},s)\supset \neg F(\vec{x},do(a,s)).
\end{eqnarray*}
Then under what Reiter called \index{the causal completeness assumption} \emph{the causal completeness assumption}, which
says that the above axioms characterize all the conditions under which
action $a$ causes $F$ to become true or false in the successor situation,
we conclude the following \emph{successor state axiom} \cite{Reiter91} \index{successor state axioms}
for fluent $F$:
\begin{equation}
\label{ssa}
F(\vec{x},do(a,s))\equiv \gamma^+(a,\vec{x},s)\lor
(F(\vec{x},s)\land \neg \gamma^-(a,\vec{x},s)),
\end{equation}
where $\gamma^+(a,\vec{x},s)$ is $\gamma^+_1(a,\vec{x},s)\lor\cdots\lor\gamma^+_m(a,\vec{x},s)$, and
$\gamma^-(a,\vec{x},s)$ is $\gamma^-_1(a,\vec{x},s)\lor\cdots\lor\gamma^-_n(a,\vec{x},s)$.

For instance, for our first blocks world, we can transform the effect axioms
about $clear(x)$ into the following axioms:
\begin{eqnarray*}
\myalign
 (\exists y.a=stack(x,y))\supset clear(x,do(a,s)),\\
\myalign
 (\exists y.a=unstack(y,x))\supset clear(x,do(a,s)),\\
\myalign
 a=putdon(x)\supset clear(x,do(a,s)),\\
\myalign
 (\exists y. a=stack(y,x))\supset \neg clear(x,do(a,s)),\\
\myalign
 (\exists y. a=unstack(x,y))\supset \neg clear(x,do(a,s)),\\
\myalign
 a=pickup(x)\supset \neg clear(x,do(a,s)).
\end{eqnarray*}
Thus we have the following successor state axiom for $clear(x)$:
\begin{eqnarray*}
\myalign\hspace*{-2em}
 clear(x,do(a,s))\equiv \\
\myalign
\exists y.a=stack(x,y)\lor 
\exists y. a=unstack(y,x)\lor
 a=putdown(x)\lor\\
\myalign
clear(x,s)\land \neg [\exists y. a=stack(y,x)\lor
 \exists y. a=unstack(x,y)\lor a=pickup(x)].
\end{eqnarray*}
Once we have a successor state axiom for each fluent in the domain, we will
then have an action theory that is complete in the same way as the 
set of axioms
(\ref{eq:blocks-world10}) - (\ref{eq:blocks-world11}) is.

This procedure can be given a
semantics in nonmonotonic logics, in particular circumscription 
\cite{McCarthy86} (see Chapter 6). This in fact has been done by 
Lin and Reiter \cite{LinReiter:constraint}.

We should also mention that for this approach to work, 
when generating the successor state axiom (\ref{ssa}) from effect axioms,
one should also assume what Reiter called \index{consistency assumption} \emph{the consistency assumption}:
the background theory should entail that $\neg(\gamma^+\land \gamma^-)$.
Once we have a set of successor state axioms, to reason with them we
need the unique names assumption about actions:
for each $n$-ary action $A$:
\[
A(x_1,...,x_n)=A(y_1,...,y_n)\supset x_1=y_1\land\cdots\land x_n=y_n,
\]
and for each distinct actions $A$ and $A'$,
\[
A(x_1,...,x_n)\neq A'(y_1,...,y_m).
\]
For more details, see \cite{Reiter91,Reiter:book}.

\subsection{The ramification problem and Lin's solution}

Recall that the frame problem is about how one can obtain a complete
axiomatization of the effects of actions from a set of
effect axioms that specifies the changes that the actions have
on the world. 
Thus Reiter's solution to the frame problem makes the assumption that
the given effect axioms characterize completely the conditions under
which an action can cause a fluent to be true or false.
However, in some action domains, providing such a complete list of
effect axioms may not be feasible. This is because in these action domains,
there are rich domain constraints \index{domain constraints} that can entail new effect axioms.
To see how domain constraints can entail new effect axioms, consider
again the blocks world. We know that each block can be at only one location:
either being held by the robot's hand, on another block, or on the table.
Thus when action $stack(x,y)$ causes $x$ to be on $y$, it also makes
$holding(x)$ false. The \index{the ramification problem} \emph{ramification problem}, first discussed by
Finger \cite{Finger86} in 1986, is about how to encode constraints like this
in an action domain, and how these constraints can be used to derive the effects of
the actions in the domain.

In the situation calculus, for a long time the only way to represent domain constraints was by
universal sentences of the form $\forall s. C(s)$. For example,
the aforementioned constraint that a block can be (and must be) at only
one location in the blocks world can be represented by the following sentences:
\begin{eqnarray*}
\myalign
 holding(x,s)\lor ontable(x,s)\lor \exists y. on(x,y),\\
\myalign
 holding(x,s)\supset \neg(ontable(x,s)\lor \exists y. on(x,y)),\\
\myalign
 ontable(x,s)\supset \neg(holding(x,s)\lor \exists y. on(x,y)),\\
\myalign
 (\exists y. on(x,y))\supset \neg (holding(x,s)\lor ontable(x,s)).
\end{eqnarray*}
So for example, these axioms and the following effect axiom about $putdown(x)$,
\[
ontable(x,do(putdown(x),s))
\]
will entail in first-order logic the following effect axiom:
\[
\neg holding(x,do(putdown(x),s)).
\]

However, domain constraints represented this way may not be strong enough
for determining the effects of actions. Consider the suitcase problem
from \cite{Lin:causality}.
Imagine a suitcase with two locks and a spring loaded mechanism
which will open the suitcase
when both of the locks are in the up position. 
Apparently, because of the spring loaded mechanism, 
if an action changes the status of the locks, then this action may also
cause, as an indirect effect, the suitcase to open.

As with the blocks world, we can represent the constraint that this spring loaded mechanism gives rise to
as the following sentence:
\begin{equation}
up(L1,s)\land up(L2,s)\supset open(s).
\label{suitcase}
\end{equation}
Although summarizing concisely
the relationship among the truth values of the three relevant propositions
at any particular instance of time, this constraint is
too weak to describe the indirect effects of actions.
For instance, suppose that initially the suitcase is
closed, the first lock in the down position, and the
second lock in the up position.
Suppose an action is then performed to turn
up the first lock. Then this constraint is ambiguous about what will
happen next. According to it, either
the suitcase may spring open or 
the second lock may get turned down. Although we have the intuition
that the former is what will happen, this constraint is not
strong enough to enforce that
because there is a different mechanism
that will yield a logically equivalent constraint.
For instance, a mechanism
that turns down the second lock
when the suitcase is closed and the first lock is up 
will yield
the following logically equivalent one:
\[
up(L1,s)\land\neg open(s)\supset \neg up(L2,s).
\]

So to faithfully represent the ramification of the
spring loaded mechanism on the effects of actions,
something stronger than the constraint
(\ref{suitcase}) is needed. 
The proposed solution by Lin \cite{Lin:causality} is to represent this
constraint as a \index{causal constraints} causal constraint:
(through the spring loaded mechanism)
the fact that both of the locks are in the up position \emph{causes}
the suitcase to open. 
To axiomatize this, Lin introduced a ternary predicate $Caused(p,v,s)$,
meaning that fluent
$p$ is caused to have truth value $v$ in situation $s$. 
The following
are some basic properties of $Caused$ \cite{Lin:causality}:
\begin{eqnarray}
\myalign Caused(p,true,s)\supset Holds(p,s),\label{causality1}\\
\myalign Caused(p,false,s)\supset \neg Holds(p,s),\label{causality2}\\
\myalign true\neq false\land (\forall v) (v=true\lor v=false),
\end{eqnarray}
where $v$ is a variable ranging over a new sort $truthValues$.

Let us illustrate how this approach works using the suitcase example.
Suppose that $flip(x)$ is an action that flips the status of the
lock $x$. Its direct effect can be described by the following axioms:
\begin{eqnarray}
\myalign up(x,s)\supset  Caused(up(x),false,do(flip(x),s)),
 \label{suitcase:direct}\\[.5ex]
\myalign \neg up(x,s)\supset 
 Caused(up(x),true,do(flip(x),s)).
 \label{suitcase:direct'}
\end{eqnarray}
Assume that $L1$ and $L2$
are the two locks on the suitcase,
the spring loaded mechanism is now represented by
the following causal rule:
\begin{equation}
up(L1,s)\land up(L2,s)\supset Caused(open,true,s).
\label{suitcase:causal}
\end{equation}
Notice that this causal rule, together with the basic axiom (\ref{causality1})
about causality, entails the
state constraint (\ref{suitcase}). Notice also that the physical,
spring loaded
mechanism behind the causal rule 
has been abstracted away. For all we care, it may just as well be that the
device is not
made of spring, but of bombs that will blow open the suitcase each
time the two locks are in the up position. It then seems natural to say
that the fluent $open$ is caused to be true by the fact that the two
locks are both in the up position.
This is an instance of what has been called \emph{static} causal rules as 
it mentions only one situation.
In comparison, causal statements
like the effect axioms
(\ref{suitcase:direct}) and (\ref{suitcase:direct'}) are
\emph{dynamic} as they mention more than one situations.

The above axioms constitute the starting theory for the domain.
To describe fully the effects of the actions, 
suitable frame axioms need to be added. Using predicate $Caused$, a generic
frame axiom can be stated as follows \cite{Lin:causality}:
Unless caused otherwise, a fluent's truth value will
persist:
\begin{equation}
 \neg (\exists v) Caused(p,v,do(a,s))\supset 
 [Holds(p,do(a,s))\equiv Holds(p,s)].
 \label{frame}
\end{equation}
For this frame axiom to make sense, one needs to minimize the
predicate $Caused$.
Technically this is done by circumscribing $Caused$ in
the above set of axioms with all
other predicates ($Poss$ and $Holds$) fixed. 
However, given the form of the axioms, this
circumscription coincides with Clark's completion of $Caused$, and it
yields the following
\emph{causation axioms}:
\begin{eqnarray}
\myalign\hspace{-3ex} Caused(open,v,s)\equiv \nonumber\\
\myalign\hspace{2em}\hspace{-3ex}  v=true\land 
  up(L1,s)\land up(L2,s), \label{suitcase:caused1} \\[.5ex]
\myalign\hspace{-3ex} Caused(up(x),v,s)\equiv \nonumber\\
\myalign\hspace{2em}\hspace{-3ex} v=true\land (\exists s')
  [s=do(flip(x),s')\land \neg up(x,s')] 
  \lor \label{suitcase:caused2} \\
\myalign\hspace{2em}\hspace{-3ex}  v=false\land (\exists s')
  [s=do(flip(x),s')\land up(x,s')].
\nonumber
\end{eqnarray}
Notice that these axioms entail the two direct effect axioms 
(\ref{suitcase:direct}, \ref{suitcase:direct'}) and the
causal rule (\ref{suitcase:causal}). 

Having computed the causal relation, the next step is to
use the frame axiom (\ref{frame})
to compute the effects of actions.
It is easy to see that from
the frame axiom (\ref{frame}) and
the two basic axioms (\ref{causality1}, \ref{causality2}) about
causality, one can infer
the following
pseudo successor state axiom:
\begin{eqnarray}
\myalign Holds(p,do(a,s))\equiv \nonumber\\
\myalign\hspace{2em} Caused(p,true,do(a,s))\lor \label{pseudoss}\\
\myalign\hspace{2em} Holds(p,s)\land \neg Caused(p,false,do(a,s)).
 \nonumber
\end{eqnarray}
From this axiom and the causation axiom
(\ref{suitcase:caused2}) for the fluent $up$,
one then obtains the
following
real successor state axiom for the
fluent $up$:
\begin{eqnarray*}
\myalign up(x,do(a,s))\equiv \\
\myalign\hspace{2em}\hspace{-.5ex} (a=flip(x)\land \neg up(x,s))\lor
(up(x,s)\land a\neq flip(x)).
\end{eqnarray*}
Similarly for the fluent $open$, we have
\begin{eqnarray*}
\myalign open(do(a,s))\equiv \\
\myalign\hspace{2em} [up(L1,do(a,s))\land up(L2,do(a,s))]\lor
 open(s).
\end{eqnarray*}
Now from this axiom,  first eliminating
$up(L1,do(a,s))$ and $up(L2,do(a,s))$ using
the successor state axiom for $up$, then using the
unique names axioms for actions, and the constraint (\ref{suitcase})
which, as we pointed out earlier, is a consequence of our axioms, we 
can deduce the following
successor state axiom for the fluent $open$:
\begin{eqnarray*}
open(do(a,s)) &\equiv&
 a=flip(L1)\land \neg up(L1,s)\land
 up(L2,s)\lor\\
&&
a=flip(L2)\land \neg up(L2,s)\land up(L1,s)\lor\\
&& open(s).
\end{eqnarray*}
Obtaining these successor state axioms solves the frame and the ramification
problems for the suitcase example.

Lin \cite{Lin:causality} showed that this procedure can be applied to a general
class of action theories, and Lin \cite{Lin:jair03} described an implemented
system that can compile these causal action theories into
Reiter's successor state axioms and STRIPS-like systems, and demonstrated the
effectiveness of the system by applying it
to many benchmark AI planning domains.
\comment{
While the approach of Lin \cite{Lin:causality} is defined directly on
the situation calculus, there have been similar proposals defined on other
formalisms (e.g. \cite{Sandewall, Turner, Thieltcher,..}).
}

\subsection{The qualification problem}

Finally, we notice that so far we have given the condition for an action $a$
to be executable in a situation $s$, $Poss(a,s)$, directly. It can be
argued that this is not a reasonable thing to do. In general, the executability
of an action may depend on the circumstances where it is performed. For instance,
we have defined $Poss(putdown(x),s)\equiv holding(x,s)$. 
But if the action is to be performed in a crowd,
then we may want to add that for the action to be executable,
the robot's hand must not be
blocked by someone; and if the robot is running low on battery, then 
we may want to ensure that the robot is not running out of battery; \emph{etc.}
It is clear that no one can anticipate all these possible circumstances,
thus no one can list all possible conditions for an action to be executable
ahead of time.
This problem of how best to specify the precondition of an action is called
the \emph{qualification problem} \index{the qualification problem}
\cite{McCarthy77}.

One possible solution to this problem is to assume that 
an action is always executable unless explicitly ruled out
by the theory. This can be achieved by maximizing the predicate $Poss$, or
in terms of circumscription, circumscribing $\neg Poss$.
If the axioms about $Poss$ all have the form
\[
Poss(A,s)\supset \varphi(s),
\]
that is, the user always provides explicit qualifications to an action,
then one can compute $Poss$ by a procedure like Clark's predicate completion
by rewriting the above axiom as:
\[
\neg \varphi(s)\supset \neg Poss(A,s).
\]
The problem becomes more complex when some domain constraints-like axioms
can influence $Poss$. This problem was first recognized by 
Ginsberg and Smith \cite{GinsbergSmith88}, and discussed in more detailed by
Lin and Reiter \cite{LinReiter:constraint}. 
For instance, we may want to add into the blocks world a constraint that
says ``only yellow blocks can be directly on the table.'' Now if
the robot is holding a red block, should she put it down on the table?
Probably she should not. 
This means that this constraint has two roles: it
rules out initial states that do not satisfy it, and it forbids agents
to perform any action that will result in a successor situation that violates
it. What this constraint should not do is to cause additional effects of
actions. For instance, it should not be the case that $putdown(x)$
would cause $x$ to become yellow just to maintain this constraint in the
successor situation. 

Lin and Reiter \cite{LinReiter:constraint} called those constraints that
yield indirect effects of actions \emph{ramification constraints}, and those
that yield additional qualifications of actions \emph{qualification 
constraints}. They are both represented as sentences of the form
$\forall s.C(s)$, and it is up to the user to classify which category
they belong to.

A uniform way of handling these two kinds of constraints is to use
Lin's causal theories of actions as described above. Under this framework,
only
constraints represented as causal rules using $Caused$ can derive new effects
of actions, and ordinary situation calculus sentences
of the form $\forall s. C(s)$ can only derive new qualifications on actions.
However, for this to work, action effect axioms like 
(\ref{suitcase:direct}) need to have $Poss$ as a precondition:
\[
Poss(flip(x),s)\supset [up(x,s)\supset  Caused(up(x),false,do(flip(x),s))],
\]
and the generic frame axiom (\ref{frame}) need to be modified similarly:
\[
 Poss(a,s)\supset \{\neg (\exists v) Caused(p,v,do(a,s))\supset 
 [Holds(p,do(a,s))\equiv Holds(p,s)]\}.
\]
In fact, this was how action effect axioms and frame axioms are represented
in \cite{Lin:causality}. An interesting observation made in \cite{Lin:causality}
was that some causal rules may give rise to both new action effects and
action qualifications.
Our presentation of Lin's causal theories in the previous subsection has 
dropped $Poss$ so that, in line with the presentation in \cite{Reiter:book},
the final successor state axioms do not have $Poss$ as a precondition.


\section{Reiter's foundational axioms and basic action theories}

We have defined the situation calculus as a first-order language with
special sorts for situations, actions, and fluents.
There are no
axioms to constrain these sorts, and all axioms are domain specific given
by the user for axiomatizing a particular dynamic system. We have used
a binary function $do(a,s)$ to denote the situation resulted from performing
$a$ in $s$, thus for a specific finite sequence of actions $a_1,...,a_k$, we
have a term denoting the situation resulted from performing the sequence
of actions in $s$: $do(a_k,do(a_{k-1},...,do(a_1,s)...))$. However, there
is no way for us to say that one situation is the result of performing
\emph{some} finite sequence of actions in another situation. This is needed for
many applications, such as planning where the achievability of a goal
is defined to be the existence of an executable finite sequence of actions that
will make the goal true
once executed. 
We now introduce Reiter's foundational axioms \index{Reiter's foundational axioms for the situation calculus} that make this possible.

Briefly, under Reiter's foundational axioms,
there is a unique initial situation, and all situations are the result
of performing some finite sequences of actions in this initial situation.
This initial situation will be denoted by
$S_0$, which formally is a constant of sort $situation$. 

It is worth mentioning here that while the constant $S_0$ has been used
before to informally stand for a starting situation, it was not assumed to be \emph{the}
starting situation as under Reiter's situation calculus. It can be said that
the difference between Reiter's version of the situation calculus and 
McCarthy's original version is that Reiter assumed the following 
foundational axioms that postulate the space of situations as a tree
with $S_0$ as the root:
\begin{eqnarray}
\myalign
do(a,s)=do(a',s')\supset a=a'\land s=s', \label{found1}\\
\myalign
\forall P. [P(S_0)\land \forall a,s. P(s)\supset P(do(a,s))]\supset
\forall s P(s). \label{found2}
\end{eqnarray}
Axiom (\ref{found2}) is a second-order induction axiom that says that
for any property $P$,
to prove that $\forall s.P(s)$, it is sufficient to show that $P(S_0)$, and
inductively, for any situation $s$, if $P(s)$ then for any action $a$,
$P(do(a,s))$. In particular, we can conclude that
\begin{itemize}
\item $S_0$ is a situation;
\item if $s$ is a situation, and $a$ an action, then $do(a,s)$ is a 
situation;
\item nothing else is a situation.
\end{itemize}
Together with the unique names axiom (\ref{found1}), this means that
we can view the domain of situations as a tree whose root is
$S_0$, and for each action $a$, $do(a,s)$ is a child of $s$. Thus
for each situation $s$ there is a unique finite sequence $\alpha$ of
actions such that $s=do(\alpha,S_0)$, where for any finite sequence $\alpha'$
of actions, and any situation $s'$, $do(\alpha',s')$ is defined inductively
as $do([],s')=s'$, and $do([a|\alpha'],s') = do(a,do(\alpha',s'))$, here we
have written a sequence in Prolog notation.
Thus there is a one-to-one correspondence between situations and finite
sequences of actions under Reiter's foundational axioms, and because of this,
Reiter identified situations with finite sequences of actions.

As we mentioned, there is a need to express assertions like ``situation $s_1$
is the result of performing a sequence of actions in $s_2$''. This is
achieved by using a partial order relation
$\sqsubset$ on situations: informally
$s\sqsubset s'$ if $s'$ is the result of performing a finite non-empty
sequence of actions in $s$.
Formally, it is defined by the following two axioms:
\begin{eqnarray}
\myalign
\neg s\sqsubset S_0, \label{found3}\\
\myalign 
s\sqsubset do(a,s')\equiv s\sqsubseteq s', \label{found4}
\end{eqnarray}
where $s\sqsubseteq s'$ is a shorthand for $s\sqsubset s'\lor s=s'$.

Notice that under the correspondence between situations and finite sequence of
actions, the partial order $\sqsubset$  is really the sub-sequence
relation: $s\sqsubset s'$ iff the action sequence of $s$ is a sub-sequence
of that of $s'$. Thus to say that a goal $g$ is achievable in situation $s$,
we write 
\[
\exists s'. s\sqsubseteq s'\land Holds(g,s')\land Executable(s,s'),
\]
where $Executable(s,s')$ means that the sequence of actions that takes
$s$ to $s'$ is executable in $s$, and is defined inductively as:
\begin{eqnarray*}
\myalign Executable(s,s),\\
\myalign Executable(s,do(a,s'))\equiv Poss(a,s')\land Executable(s,s').
\end{eqnarray*}

Reiter's foundational axioms (\ref{found1}) - (\ref{found4})
make it possible to formally prove 
%in what Reiter called \emph{the} the situation calculus 
many interesting properties
such as the achievability of a goal. They also lay the foundation for
using the situation calculus to formalize strategic and control
information (see e.g. \cite{Lin:cut,Lin:search}). They are particularly
useful in conjunction with Reiter's successor state axioms, and 
are part of what Reiter called the \emph{basic action theories} as we 
proceed to describe now.

To define \index{basic action theories} Reiter's basic action theories, we first need to define the notion
of \index{uniform formulas} \emph{uniform formulas}. Intuitively, if $\sigma$ is a situation term,
then a formula is uniform in $\sigma$ if the truth value of the formula
depends only on $\sigma$.
Formally, a situation
calculus formula is uniform in $\sigma$ if it satisfies the following
conditions:
\begin{itemize}
\item it does not contain any quantification over situation;
\item it does not mention any variables for relational fluents;
\item it does not mention any situation term other than $\sigma$;
\item it does not mention any predicate that has a situation 
argument other than $Holds$; and
\item it does not mention any function that has a situation argument
unless the function is a functional fluent.
\end{itemize}
Thus $clear(x,s)$ is uniform in $s$ (recall that this is a shorthand for
$Holds(clear(x),s)$), but $\forall s. clear(x,s)$ is not as it 
quantifies over situations. The formula $\forall p. Holds(p,s)$ is
not uniform in $s$ either as it contains $p$ which is a variable for
relational fluents.
Notice that a uniform formula cannot
mention domain-independent situation-dependent predicates like $Poss$,
$\sqsubset$, and $Caused$. It cannot even contain equalities between
situations such as $s=s$, but it can contain equalities between actions and
between domain objects
such as $x\neq y$, where $x$ and $y$ are variables of sort $block$ in the
blocks world.

Another way to view uniform formulas is by using a first-order language 
without the special $situation$ sort. The predicates of this language are
relational fluents and other situation independent predicates. The
functions are functional fluents, actions, and other situation independent
functions. A situation calculus formula $\Phi$ is uniform in $\sigma$ iff
there is a formula $\varphi$ in this language such that $\Phi$ is the result
of replacing every relational fluent atom $F(t_1,...,t_k)$ in 
$\varphi$
by $Holds(F(t_1,...,t_k),\sigma)$ (or $F(t_1,...,t_k,\sigma)$)
 and every functional fluent term $f(t_1,...,t_k)$ by
$f(t_1,...,t_k,\sigma)$.
In the following, and in Chapter 24 on Cognitive Robotics, this formula
$\Phi$ is written as $\varphi[\sigma]$.

Uniform formulas are used in Reiter's action precondition axioms and 
successor state axioms. In Reiter's basic action theories, an action
precondition axiom \index{action precondition axioms} for an action $A(x_1,...,x_n)$ is a sentence of the form:
\[
Poss(A(x_1,...,x_n),s)\equiv \Pi(x_1,...,x_n,s),
\]
where $\Pi(x_1,...,x_n,s)$ is a formula uniform in $s$ and whose free variables
are among $x_1,...,x_n,s$. Thus whether $A(x_1,...,x_n)$ can be performed
in a situation $s$ depends entirely on $s$.

We have seen successor state axioms for relational fluents (\ref{ssa}).
In general, in Reiter's basic action theories,
a successor state axiom \index{successor state axioms} for 
an $n$-ary relational fluent $F$ is a sentence of the form
\begin{equation}
\label{ssa1}
F(x_1,...,x_n,do(a,s))\equiv \Phi_F(x_1,...,x_n,a,s),
\end{equation}
where $\Phi_F$ is a formula uniform in $s$, and whose free variables are among
$x_1,...,x_n,a,s$. 
%Compared with (\ref{ssa}), this axiom does not have
%$Poss(a,s)$ as a condition. In solving the frame, ramification, and
%qualification problems, it is important to condition the effect axioms
%on $Poss(a,s)$ as this will allow us to derive implicit action
%preconditions. From these effect axioms, we can only derive successor
%state axioms of the form (\ref{ssa}). However, once we have solved
%the qualification problem and have an action precondition axiom for
%each action, then there is no need to keep $Poss(a,s)$ as a condition
%in successor state axioms. This is because, whenever needed, 
%we can always ensure
%that $Poss(a,s)$ is true when we need to consider the truth values of fluents
%in $do(a,s)$. 
%Reiter's basic action theories can be considered a parsimonious
%representation for a solution to the frame and related problems.
%They do not assume how these problems are solved and are
%meant to be the starting point to
%solve the reasoning problems such as planning in dynamic systems.
%Dropping the condition $Poss(a,s)$ simplifies successor state axioms
%as well as the statements and proofs of many theorems about Reiter's
%basic action theories.

Similarly, if $f$ is an $(n+1)$-ary functional fluent, then a successor state axiom for it
is a sentence of the form
\begin{equation}
\label{ssa2}
f(x_1,...,x_n,do(a,s))=v\equiv \varphi(x_1,...,x_n,v,a,s),
\end{equation}
where $\varphi$ is a formula uniform in $s$, and whose free variables are among
$x_1,...,x_n,v,a,s$.

Notice that requiring the formulas $\Phi_F$ and $\varphi$ in successor state
axioms to be uniform amounts to making Markov assumption in systems and
control theory: the effect of an action depends only on the current situation.

We can now define Reiter's basic action theories
\cite{Reiter:book}. A basic action theory $\mathcal D$ is a 
set of axioms
of the following form:
\[
\Sigma\cup {\mathcal D}_{ss}\cup {\mathcal D}_{ap}\cup {\mathcal D}_{una}\cup {\mathcal D}_{S_0},
\]
where
\begin{itemize}
\item $\Sigma$ is the set of the four foundational axioms (\ref{found1}) - (\ref{found4}).
\item ${\mathcal D}_{ss}$ is a set of successor state axioms. It must
satisfy the following \emph{functional fluent consistency property}:
if (\ref{ssa2}) is in ${\mathcal D}_{ss}$, then
\[
\hspace*{-2.6em}{\mathcal D}_{una}\cup {\mathcal D}_{S_0}\models
\forall \vec{x}. \exists v\varphi(\vec{x},v,a,s)\land
[\forall v,v'. \varphi(\vec{x},v,a,s)\land \varphi(\vec{x},v',a,s)\supset
v=v'].
\]
\item ${\mathcal D}_{ap}$ is a set of action precondition axioms.
\item ${\mathcal D}_{una}$ is the set of unique names axioms
about actions.
\item ${\mathcal D}_{S_0}$ is a set of sentences that are uniform in 
$S_0$. This is the knowledge base for the initial situation $S_0$.
\end{itemize}

The following theorem is proved by Pirri and Reiter \cite{PirriReiter99}.
\begin{theorem}[Relative Satisfiability]
A basic action theory $\mathcal D$ is satisfiable iff 
${\mathcal D}_{una}\cup {\mathcal D}_{S_0}$ is.
\end{theorem}

As we mentioned above, the basic action theories are the starting point
to solve various problems in dynamic systems. Many of these problems can
be solved using basic action theories by first-order deduction. But some
of them require induction. Those that require induction are typically about
proving general assertions of the form $\forall s.C(s)$, such as proving
that a certain goal is not achievable. For instance, consider the basic
action theory ${\mathcal D}$ where ${\mathcal D}_{ap}=\emptyset$,
${\mathcal D}_{ss} = \{ 
\forall a,s. loaded(do(a,s))\equiv loaded(s) \}$,
and ${\mathcal D}_{S_0} = \{ loaded(S_0)\}$. It is certainly true that
${\mathcal D}\models \forall s. loaded(s)$. But proving this formally
requires induction.

The ones that can be done in first-order logic include checking whether
a sequence of ground actions is executable in $S_0$ and the temporal projection
problem, which asks whether a formula holds after a sequence of actions
is performed in $S_0$. One very effective tool for solving these problems
is \index{regression} \emph{regression},\footnote{Reiter \cite{Reiter:book} defined regression for a more general class of formulas that can contain
$Poss$ atoms.} which transforms a formula
\[
\varphi(do([\alpha_1,...,\alpha_n],S_0))\]
 that is uniform in
$do([\alpha_1,...,\alpha_n],S_0)$
to a formula $\varphi'(S_0)$
that is uniform in $S_0$ such that 
\[
{\mathcal D}\models \varphi(do([\alpha_1,...,\alpha_n],S_0)) \mbox{ iff }
{\mathcal D}_{una}\cup {\mathcal D}_{S_0}\models \varphi'(S_0).
\]
If $\varphi(do([\alpha_1,...,\alpha_n],S_0))$ does not have 
functional fluents, then the regression can be defined inductively as 
follows: the regression of $\varphi(S_0)$ is $\varphi(S_0)$, and
inductively, if $\alpha$ is an action term, and $\sigma$ a
situation term, then the regression of $\varphi(do(\alpha,\sigma))$ is
the regression of the formula obtained
by replacing in $\varphi(do(\alpha,\sigma))$ each relational
fluent atom $F(\vec{t},do(\alpha,\sigma))$ by $\Phi_F(\vec{t},\alpha,\sigma)$,
where $\Phi_F$ is the formula in the right side of the successor state
axiom (\ref{ssa1}) for $F$. When $\varphi$ contains functional fluents,
the definition of regression is more involved, see \cite{Reiter:book}.

For instance, given the following successor state axioms:
\begin{eqnarray*}
\myalign
F(do(a,s))\equiv a=A\lor F(s),\\
\myalign
G(do(a,s))\equiv (a=B\land F(s))\lor G(s),
\end{eqnarray*}
the regression of $G(do(B,do(A,S_0)))$ is the regression of
\[
(B=B\land F(do(A,S_0)))\lor G(do(A,S_0)),
\]
which is the following sentence about $S_0$:
\[
(B=B\land (A=A\lor F(S_0)))\lor (A=B\land F(S_0))\lor G(S_0),
\]
which is equivalent to $true$.

Using regression, we can check the executability of a sequence of
actions in $S_0$, say $[stack(A,B),pickup(C),putdown(C)]$, as follows:
\begin{enumerate}
\item This sequence of actions is executable in $S_0$ iff the following
formulas are entailed by $\mathcal D$:
\begin{eqnarray*}
\myalign Poss(stack(A,B),S_0),\\
\myalign Poss(pickup(C), do(stack(A,B),S_0)),\\
\myalign Poss(putdown(C), do(pickup(C), do(stack(A,B),S_0))).
\end{eqnarray*}
\item Use action precondition axioms to rewrite the above sentences into
uniform sentences. For instance, the first two sentences can be rewritten
into the following sentences:
\begin{eqnarray*}
\myalign clear(B,S_0)\land holding(A,S_0),\\
\myalign handempty(do(stack(A,B),S_0)) \land ontable(C,(do(stack(A,B),S_0)))\land
\\
\myalign\hspace*{3em} clear(C,(do(stack(A,B),S_0))).
\end{eqnarray*}
\item Regress the uniform
sentences obtained in step 2, and check whether the regressed formulas
are entailed by ${\mathcal D}_{una}\cup {\mathcal D}_{S_0}$.
\end{enumerate}

\section{Applications}

The situation calculus provides a rich framework for solving problems in
dynamic systems. Indeed, Reiter 
\cite{Reiter:book} showed that many such problems can be formulated
in the situation calculus and solved
using a formal situation calculus specification. He even had the
slogan ``No implementation without a
sitcalc specification.''

The first application of the situation calculus is in planning
where an agent
needs to figure out a course of actions that will achieve a given goal.
Green \cite{Green69} formulated this problem as a theorem
proving task in the situation calculus:
\[
T\models \exists s. G(s),
\]
where $T$ is the situation calculus theory for the planning problem, and $G$
the goal.
Green's idea was that if one can find a proof of the above theorem constructively,
then a plan can be read off from the witness situation term in the proof. He
actually implemented
a planning system based on this idea using a first-order theorem
prover. For various reasons, the system could solve only extremely simple problems.
Some researchers believe that
Green's idea is correct. What one needs is a good way to encode domain
specific control knowledge as the situation calculus sentences to direct
the theorem prover intelligently.

One reason that Green's system performed poorly was that the theory $T$ that
encodes the planning problem is not very effective. Assuming that the planning
problem is specified by a basic action theory, Reiter implemented a planner
in Prolog that can efficiently make use of domain-specific control
information like that in \cite{BK2000}. It can even do open-world
planning where the initial situation is not completely specified. For more
details see \cite{Reiter:book}.

The situation calculus has also been used to formalize and reason about 
computer programs.
Burstall used it 
to formalize Algol-like programs \cite{Burstall69}.
Manna and Waldinger used it to formalize general assignments in Algol 68
\cite{MannaWaldinger81}, and later Lisp imperative 
programs \cite{MannaWaldinger87}.

More recently, Lin and Reiter used it to axiomatize logic programs with
negation-as-failure \cite{LinReiter:lp}. The basic idea is as follows.
A rule
(clause) $P \leftarrow G$ means that whenever $G$ is proved, we can use this
rule to prove $P$. Thus we can name this rule by an action so that the
consequence of the rule becomes the effect of the action, and the
body of the rule becomes the context under which the action will have
the effect.\footnote{Alternatively, one could also view the body of a
rule as the precondition of the corresponding action.} 
Formally, for each rule
\[
F(t_1,...,t_n) \leftarrow Q_1,...,Q_k, \mbox{not }Q_{k+1},..., \mbox{not }Q_m
\]
Lin and Reiter introduced a corresponding
$n$-ary action $A$, and axiomatized it with the following axioms:
\begin{eqnarray*}
&\hspace*{-3em}&
Poss(A(\vec{x}),s),\\
&\hspace*{-3em}&
[\exists \vec{y_1}Holds(Q_1,s)\land\cdots\land
\exists \vec{y_k}Holds(Q_k,s)\land
\neg(\exists \vec{y_{k+1}},s)Holds(Q_{k+1},s)\land\cdots\land\\
&\hspace*{-3em}&\hspace{2em}
\neg(\exists \vec{y_m},s)Holds(Q_m,s)]\supset 
F(t_1,...,t_n,do(A(\vec{x}),s)),
\end{eqnarray*}
where $\vec{y_i}$ is the tuple of variables in $Q_i$ but not in
$F(t_1,...,t_n)$.

Notice that $\neg(\exists \vec{y_i},s)Holds(Q_i,s)$ means that the goal
$Q_i$ is not achievable (provable) no matter how one instantiate the
variables that are in $Q_i$ but not in the head of the rule. This is
meant to capture the
``negation-as-failure'' feature of the operator ``not'' in logic
programming.

Now for a logic program $\Pi$, which is a finite set of rules, one can 
apply Reiter's solution to the effect axioms obtained this way for all rules
in $\Pi$, and obtain a set of successor state axioms, one for each
predicate occurring in the program.\footnote{If a predicate does not
occur as the head of a rule, then add an axiom to say that this relation
does not hold for any situation.}
Thus for each program $\Pi$, we have a corresponding basic action
theory\footnote{Strictly speaking, it is not a basic action theory as
the right side of a successor state axiom may contain $\exists s.Q(s)$
when there is a negation in front of $Q$ in a rule, thus is not a uniform
formula.} $\mathcal D$ for it with 
\[
{\mathcal D}_{S_0}=
\{ F(\vec{x},S_0)\equiv false\D F \mbox{ is a predicate in $\Pi$}\}.\]
In other words, in the initial situation, all fluents are false.
Now query answering in a logic program becomes planning under the
corresponding basic action theory.

As it turned out, this formalization of logic programs in the situation
calculus yields a semantics that is equivalent to
Gelfond and Lifschitz's stable model semantics.
This situation calculus semantics can be used to
formally study some interesting properties of logic programs. For instance,
it can be proved that program unfolding preserves this
semantics. More interestingly, under this semantics and Reiter's
foundational axioms, derivations under a program are isomorphic to
situations. Thus those operators that constrain derivations
in logic programming can be
axiomatized in the situations calculus by their 
corresponding constraints on situations. 
Based on this idea, Lin proposed a situation
calculus semantics for
the ``cut'' operator in logic programming \cite{Lin:cut}.

The most significant application so far is the use of the situation calculus
as a working language for Cognitive Robotics. For details about this
application, the reader is referred to the chapter on Cognitive Robotics
in this Handbook.


\section{Concluding remarks}

What we have described so far is just the elemental of the situation
calculus. The only thing that we care about an action so far is its
logical effects on the physical environment. We have ignored many
other aspects of actions, such as their durations and their effects on the
agent's mental state. We have also assumed that actions
are performed sequentially one at a time and that they are the only force
that may change the state of the world. 
%Some had cited these as evidence
%of the inadequacy of the situation calculus as a formalism for representing
%change. 
These and other issues in reasoning about action have been addressed in
the situation calculus, primarily as a result of
using the situation
calculus as the working language for Cognitive Robotics. We refer the
interested readers to Chapter 24 and \cite{Reiter:book}.

\section{Acknowledgements}

I would like to thank Gerhard Lakemeyer, Hector Levesque, and Abhaya Nayak
for their very useful
comments on an earlier version of this article.

\bibliography{../Latex-Bib/ref}


\end{document}