%April 13, 1999
%Feb 2002 for JAIR
%Revised in Toronto in March 2003
%Anothe revision: May 15, 2003. Toronto.
%Final revision: Sept, 2003. Hong Kong


\documentstyle[jair,twoside,11pt,theapa]{article}
\input epsf %% at top of file

\jairheading{19}{2003}{279-314}{09/02}{10/03}
\ShortHeadings{From Causal Theories to STRIPS-Like Systems}
{Lin}
\firstpageno{279}

\newcommand{\var}{\varphi}
\newcommand{\D}{\:\: |\:\:}
\newcommand{\ttl}{\subsubsection*}
\newcommand{\rto}{\rightarrow}
\newcommand{\lto}{\leftarrow}
\newtheorem{definition}{Definition}
\newtheorem{examp}{Example}
\newenvironment{example}{\begin{examp}\rm}{\end{examp}}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newenvironment{proof}{{\bf Proof:}}{{\hfill $\Box$}\\ }
\newenvironment{lprule}{\begin{center}\tt\begin{tabular}{rl}}{\end{tabular}\end{center}}
\newenvironment{smallenu}{\begin{enumerate}\setlength{\itemsep}{0.0pt}}{\end{enumerate}}
\newenvironment{smallitem}{\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{\is}{\stackrel{\triangle}{=}}
\newcommand{\mif}{{\bf if}}
\newcommand{\mwhile}{{\bf while}}
\newcommand{\mthen}{{\bf then}}
\newcommand{\melse}{{\bf else}}
\newcommand{\mdo}{{\bf do}}
%\newcommand{\mand}{\!\circ\!}
\newcommand{\mand}{\;\mbox{\tt\&}\;}
\newcommand{\cut}{\mbox{\tt !}}
\newcommand{\less}{\prec}
\newcommand{\sa}{same\mbox{-}actions}
\newcommand{\firstproof}{\mbox{\tt first-der}}
\newcommand{\minimal}{\mbox{\tt minimal}}
\newcommand{\Holds}{H}
\newcommand{\holds}{H}
\newcommand{\Poss}{Poss}
\newcommand{\acc}{Acc}
\newcommand{\caused}{Caused}
\newcommand{\effect}{E\!f\!\!f\!ect}
\newcommand{\action}{Action}
\newcommand{\fluent}{F\!luent}
\newcommand{\complex}{Complex}
\newcommand{\defined}{De\!f\!ined}
\newcommand{\static}{Static}
\newcommand{\axiom}{Axiom}
\newcommand{\causes}{Causes}
\newcommand{\poss}{Precond}
\newcommand{\domain}{Domain}


\title{Compiling Causal Theories to Successor State Axioms and
STRIPS-Like Systems}
\author{\name Fangzhen Lin \email flin@cs.ust.hk\\
\addr Department of Computer Science\\
The Hong Kong University of Science and Technology\\
Clear Water Bay, Kowloon, Hong Kong
}

\begin{document}
\maketitle

%\begin{center}
%Draft of July 12, 1999\\[5ex]
%\end{center}

\begin{abstract}
We
describe a system for specifying the effects of actions.
Unlike those
commonly used in AI planning,
our system uses an action description language that
allows one to specify the effects of actions using domain rules, which are
state constraints that
can entail new action effects from old ones.
Declaratively, 
an action domain in our language corresponds to
a nonmonotonic causal theory in the situation calculus.
Procedurally,
such an action domain is compiled into a set of
logical theories, one for each action in the domain, from which
fully instantiated
successor state-like axioms and STRIPS-like systems are then generated.
We expect the system to be a useful tool for knowledge engineers writing
action specifications for classical AI
planning systems, GOLOG systems, and other systems where formal
specifications of actions are needed.
\end{abstract}








\section{Introduction}

We describe a system for generating action effect specifications
from a set of domain rules and direct action effect axioms, among other things.
We expect the system to be a useful tool for knowledge engineers writing
action specifications for classical AI
planning systems, GOLOG systems \shortcite{golog}, and other systems where formal
specifications of actions are needed.

To motivate, consider the language used by STRIPS \cite{FikesNilsson71}
for describing the effects of actions.
Briefly speaking, an action is described in this language by a first-order
formula, called its precondition that describes the condition
under which the action
is executable, an add list that enumerates the propositions
that the action will
make true when successfully executed in a situation, and a delete list 
that enumerates the propositions that the action
will make false when successfully executed in a situation.
While the original STRIPS allowed the precondition and
the elements of the two lists to be complex formulas, STRIPS actions now
refer only to those whose precondition is given by a conjunction of atomic
formulas and whose add and delete lists are lists of atomic formulas. It
is widely acknowledged that this language is inadequate for describing
actions in the real world. One of the limitations, the one that we address
in this paper, is that with the language, one has to enumerate all possible
effects of an action, a difficult if not impossible task for complex
domains.
For example, given a large C program, it is hard to figure out the effects
of changing the value of a pointer on the values of all other pointers
in the program. 
However, the underlying principle is very simple: when the value
of a pointer changes, the values of all other pointers that point to the
same memory location change as well. Put another way, the direct 
effect of the action of changing the value of a pointer to $x$ is that the
value of the pointer will be $x$. The indirect or side effects of this
action are those derived from the constraint which says that 
if two pointers point to
a common location, then their values must be the same.

This idea of specifying the effects of actions using domain constraints is like
``engineering from first principle'', and has many advantages.
First of all,
constraints are action independent, and work on all
actions.
Secondly, if the effects of actions derived from domain constraints
agree with one's expectation, then this will be a good indication that one
has axiomatized the domain correctly.
Finally, domain constraints can be used for other purposes as well.
For instance, they can be used to check the consistency of the initial
situation database. In general, when a set of sentences violates a domain
constraint, we know that no legal situation can satisfy this set of
sentences. This idea can and has been used in planning to prune impossible
states. Recently, there have even been efforts at ``reverse engineering''
domain constraints from STRIPS-like systems 
to speed up planners \cite<e.g.>[and others]{ZhangFoo97,GereviniSchubert98,FoxLong98}.


While it is appealing to use domain constraints to derive
the indirect effects of actions, making the idea work
formally turned out to be
a challenge. The problem is commonly known as the ramification problem,
and various proposals have been made to solve it.
Until recently, however, these proposals were at best of theoretical interest
only because of their high computational complexity.
The situation has since changed substantially due to the use of causality in
representing domain constraints \cite[and others]{Lin:causality,Lin:aaai96,McCainTurner95,McCainTurner97,Thielscher95,Thielscher97,Baral95,Lifschitz97}.
What we will describe in this paper is an implemented
system that builds on this recent work on causality-based approaches to
the ramification problem. Specifically, our system
takes as input an action domain description where 
actions are described by their
precondition axioms and direct effect axioms, and domain constraints are
represented by what we call {\em domain rules}. The system returns
as output a complete
action specification both in STRIPS-like format and
as a set of fully instantiated successor state axioms
\cite{Reiter91}. 

This paper is organized as follows.
We begin by
introducing our action description
language.
We then propose a procedure to compile an action domain specified in this
language into
a complete
set of successor state axioms from which a STRIPS-like description
is then extracted. We then show the soundness of this procedure with
respect to a translation from action domain descriptions to 
situation calculus causal theories of \citeA{Lin:causality}.
We next describe an implementation
of this procedure, and present some experimental results. 
As one will see, one of the limitations of our system
is that it is essentially propositional. While effect axioms and domain
rules can have variables, they need to be fully instantiated during the
compilation process. To partially overcome this limitation, we show
some results that allow one to generalize the propositional output to
the first-order case for certain classes of action domain descriptions.
We then discuss some related work, and conclude this paper with some pointers
for future work.


\section{An Action Description Language}

We assume a first-order language with equality.
We shall call those predicates whose extensions 
may be changed by actions {\em fluents}, and those whose extensions
are not changed by any actions {\em static relations}. We also call
unary static relations {\em types}.
By  {\em fluent atoms} 
we mean those atomic formulas formed by fluents. An {\em equality} atom
is one of the form $u=v$, where $u$ and $v$ are variables or constants, 
and an inequality
constraint is one of the form $u\neq v$.
Actions are represented by functions, and they are assumed to be the
only functions with positive arities in the language.

Our action description language includes the following components.

\subsection{Type Definitions}

A type definition is specified by expressions of the following form:
\[ \domain(p, \{ a_1,...,a_n\}),
\]
where $p$ is a type, and $a_1,...,a_n$ are constants. The
intuitive meaning of this expression is that the domain (extension)
of the type
$p$ is the set $\{ a_1,...,a_n\}$.
For instance, in the blocks world, we may have a type called $block$,
and have, say, five blocks named numerically:
$\domain(block, \{ 1,2,3,4,5\})$. 
In a logistics domain, we may have a type called
$loc$ for locations, and have, say, 3 locations $l_1$, $l_2$, and $l_3$:
$\domain(loc, \{ l_1,l_2,l_3\})$.
%We remark here that our current system requires the domain of a type to
%be finite and explicitly enumerated, in order to keep things at a propositional
%level.

\subsection{Primitive Fluent Definitions}

Primitive fluents are defined by expressions of the following form:
\[
\fluent(f(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\land\cdots
 \land e_m),
\]
where $f$ is an n-ary fluent, each $p_i$, $1\leq i\leq n$, 
a type, and each $e_i$, $1\leq i\leq m$, an inequality constraint of the form
$x_j\neq x_k$, for some $1\leq j < k\leq n$. 
The intuitive meaning of this expression is that
$f(x_1,...,x_n)$ is a legal 
fluent atom if the second argument is true. For instance,
in the blocks world, given the type definition
$\domain(block, \{ 1,2,3\})$, the following fluent specification:
\[
\fluent(on(x,y), block(x)\land block(y)\land x\neq y)
\]
would generate the following six legal fluent atoms:
\[
on(1,2), on(1,3), on(2,1), on(2,3), on(3,1), on(3,2).
\]
Clearly, there should be exactly one fluent definition for each fluent.

\subsection{Complex Fluent Definitions}

Given a set of primitive fluents, one may want to define some new ones.
For instance, in the blocks world, given the primitive fluent $on$,
we can define $clear$ in terms of $on$ as: 
$(\forall x) clear(x)\equiv \neg (\exists y)on(y,x)$.

To specify complex fluents like $clear$,
 we first define {\em fluent formulas} as follows:
\begin{itemize}
\item $t_1=t_2$ is a fluent formula, where $t_1$ and $t_2$ are terms, i.e.
either a constant in the domain of a type or a variable.
\item $f(t_1,...,t_n)$ is a fluent formula, where $t_1,...,t_n$ are terms,
and $f$ is either an n-ary primitive fluent, a complex fluent, or
a static relation.
\item If $\var$ and $\var'$ are fluent formula, then $\neg \var$,
$\var\lor \var'$, $\var\land\var'$, $\var\supset\var'$, and
$\var\equiv\var'$
are also fluent formulas.
\item If $\var$ is a fluent formula, $x$ a variable, and $p$ a type,
then  $\forall (x,p)\var$ (for all $x$ of type $p$, $\var$ holds) and 
$\exists (x,p)\var$ (for some $x$ of type $p$, $\var$ holds) are fluent
formulas. Notice that we require types to have finite domains, so
these quantifications are really shorthands: If the domain of $p$ is
$\{a_1,...,a_n\}$, then $\forall (x,p)\var$ stands for
\[
\var(x/a_1)\land\cdots\land \var(x/a_n),
\]
and $\exists (x,p)\var$ stands for
\[
\var(x/a_1)\lor\cdots\lor \var(x/a_n).
\]
\end{itemize}

A complex fluent is then specified in our language by a pair of expressions
of the following form:
\begin{eqnarray*}
\align
\complex(f(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\cdots\land e_m),\\
\align \defined(f(x_1,...,x_n), \var),
\end{eqnarray*}
where $p_i$'s and $e_i$'s are the same as in primitive fluent definitions,
and
$\var$ a fluent formula that does not mention any complex
fluents and whose free variables are among $x_1,...,x_n$.
The first expression specifies the syntax and the second the semantics
of the complex fluent.

For instance, the complex fluent $clear$ in the blocks world can be
specified as:
\begin{eqnarray*}
\align \complex(clear(x), block(x)),\\
\align
\defined(clear(x), \neg \exists (y, block)on(y,x)).
\end{eqnarray*}
As we mentioned above, quantifiers here are just
shorthands because each type must have a finite domain.
For instance, given the following specification:
\begin{eqnarray*}
\align \domain(block, \{1,2,3\}),\\
\align \fluent(on(x,y), block(x)\land block(y))
\end{eqnarray*}
the above fluent definition for $clear$ will be expanded to:
\begin{eqnarray*}
\align \defined(clear(1),  \neg(on(1,1)\lor on(2,1)\lor on(3,1))),\\
\align \defined(clear(2),  \neg(on(1,2)\lor on(2,2)\lor on(3,2))),\\
\align \defined(clear(3),  \neg(on(1,3)\lor on(2,3)\lor on(3,3))).
\end{eqnarray*}

\subsection{Static Relation Definitions}

As we mentioned, a static relation is one that is not changed by any action in
the domain. For instance, in the robot navigation domain, we may have
a proposition $connected(d,r1,r2)$ meaning that door $d$ connects rooms
$r1$ and $r2$. The truth value of this proposition cannot be changed by 
the navigating robot that just rolls from room to room.

In our language, a static relation
is defined by an expression of the following
form:
\[
\static(g(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\land\cdots
 \land e_m),
\]
where $g$ is an n-ary predicate, and
$p_i$'s and $e_i$'s are the same as in primitive fluent definitions.
The meaning of this expression is similar to a
fluent definition, and there should be exactly one definition for each
static relation.

\subsection{Domain Axioms}

Domain axioms are constraints on static relations. For instance, for
the static proposition $connected(d,r1,r2)$, we may want to impose the
following constraint:
$connected(d,r1,r2)\equiv connected(d,r2,r1)$.
In our language, domain axioms are specified by expressions of the
form:
\[
\axiom(\var),
\]
where $\var$ is a fluent
formula that does not mention any
fluents, i.e. it mentions only static relations and equality.
For instance, the above constraint on $connected$ is written
as:
\begin{eqnarray*}
\align
\axiom(\forall (d, door)\forall(r_1, room)\forall (r_2,room)
 connected(d,r_1,r_2)\equiv\\
\align \hspace*{2em} connected(d,r_2,r_1)),
\end{eqnarray*}
where $door$ and $room$ are types.


\subsection{Action Definitions}

Actions are defined by expressions of the following form:
\[
\action(a(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\land\cdots
\land e_m),
\]
where $a$ is an n-ary action, and $p_i$'s and $e_i$'s are the same as
in primitive fluent definitions.
For instance,
in the blocks world, given the type definition
$\domain(block, \{ 1,2,3\})$, the following action specification:
\[
\action(stack(x,y), block(x)\land block(y)\land x\neq y)
\]
would generate the following six action instances:
\[
stack(1,2), stack(1,3), stack(2,1), stack(2,3), stack(3,1), stack(3,2).
\]
There should be exactly one action definition for each action.

\subsection{Action Precondition Definitions}

Action precondition definitions
are specified by expressions of the following form:
\[
\poss(a(x_1,...,x_n), \var),
\]
where $a$ is an n-ary action, $\var$ is a fluent formula whose free
variables are among $x_1,...,x_n$.

There should be exactly one precondition definition for each action.
For instance, in
the blocks world, we may have:
\[
 \poss(stack(x,y), clear(x)\land clear(y)\land ontable(x)),
\]
which says that for the action $stack(x,y)$ to be executable in a situation,
$clear(x)$, $clear(y)$, and $ontable(x)$ must be true in it.

\subsection{Action Effect Specifications}

Action effects are specified by expressions of the following form:
\[
\effect(a(x_1,...,x_n), \var, f(y_1,...,y_k)),
\]
or of the form:
\[
\effect(a(x_1,...,x_n), \var, \neg f(y_1,...,y_k)),
\]
where $\var$ is a fluent formula, and $f$ a primitive fluent.
The intuitive meaning of these 
expressions is that if $\var$ is true in the initial situation, then
action $a(x_1,...,x_n)$ will cause $f(y_1,...,y_k)$ to be true (false).
For instance, in the blocks world, action $stack(x,y)$ causes $x$ to
be on $y$:
\[ \effect(stack(x,y), true, on(x,y)).
\]
For an example of a context dependent effect, consider action $drop(x)$ that 
breaks an object only if it is fragile:
\[
\effect(drop(x), fragile(x), broken(x)).
\]

Notice here that the fluent formula $\var$ in the action effect specifications
can have variables that are not in
$x_1,...,x_n,y_1,...,y_k$. Informally, all the variables are supposed
to be ``universally quantified.'' More precisely, when these
expressions are instantiated, one can substitute any objects
for these variables, provided the resulting
formulas are well-formed. For instance, given the action
effect specification $\effect(move(x), g(x_1)\land q(x_1,x_2), f(y))$,
one can instantiate it to: $\effect(move(a), g(b)\land q(b,c), f(d))$,
as long as $move(a)$ is a legal action (according to the action
definition for $move$)
and $g(b)$, $q(b,c)$, and $f(d)$ are legal fluent atoms (according to the
fluent definitions for $g$, $q$, and $f$).

\subsection{Domain Rules}

Domain rules are specified by expressions of the following form:
\[
\causes(\var, f(x_1,...,x_n)),
\]
or of the following form:
\[
\causes(\var, \neg f(x_1,...,x_n)),
\]
where $\var$ is a fluent formula, and $f$ a primitive fluent. Like
action effect specifications, $\var$ here can have variables that are
not in $x_1,...,x_n$.
The intuitive meaning of a domain
rule is that in any situation, if $\var$ holds, then the fluent atom
$f(x_1,...,x_n)$ will be caused to be true. A domain rule is stronger
than material implication. Its formal semantics is given by
mapping it to a causal rule of \citeA{Lin:causality} 
(see Section~\ref{formal-semantics}), thus the
name ``causes''.
For instance, in
the blocks world, a block can be on only one other block:
\[
\causes(on(x,y)\land y\neq z, \neg on(x,z)).
\]
In a logistics domain, one may want to say that 
if a package is inside a truck which is at
location $l$, then the package is at location $l$ as well:
\[
\causes(in(x,y)\land at(y,l), at(x,l)).
\]

\subsection{Action Domain Descriptions}

The following definition sums up our action description language:

\begin{definition}
An {\em action domain description}
is a set of type definitions, 
primitive fluent definitions, complex fluent definitions,
static proposition definitions, domain axioms,
action definitions, action precondition definitions, action
effect specifications, and domain rules.
\end{definition}


\begin{example}
\label{example}
The following action domain description defines a blocks world with three
blocks:
\begin{eqnarray*}
\align \domain(block, \{ 1,2,3\}),\\
\align
\fluent(on(x,y), block(x)\land block(y)),\\
\align
\fluent(ontable(x), block(x)),\\
\align \complex(clear(x), block(x)),\\
\align \defined(clear(x), \neg \exists (y, block)on(y,x)),\\[1ex]
\align
\causes(on(x,y)\land x\neq z, \neg on(z,y)),\\
\align
\causes(on(x,y)\land y\neq z, \neg on(x,z)),\\
\align
\causes(on(x,y), \neg ontable(x)),\\
\align
\causes(ontable(x), \neg on(x,y)),\\[1ex]
\align
\action(stack(x,y), block(x)\land block(y)\land x\neq y),\\
\align
\poss(stack(x,y),ontable(x)\land clear(x)\land clear(y)),\\
\align
\effect(stack(x,y),true,on(x,y)),\\[1ex]
\align
\action(unstack(x,y), block(x)\land block(y)\land x\neq y),\\
\align
\poss(unstack(x,y),clear(x)\land on(x,y)),\\
\align
\effect(unstack(x,y),true,ontable(x)),\\[1ex]
\align
\action(move(x,y,z), block(x)\land block(y)\land block(z)\land x\neq y
\land x\neq z\land y\neq z),\\
\align
\poss(move(x,y,z),on(x,y)\land clear(x)\land clear(z)),\\
\align
\effect(move(x,y,z),true,on(x,z)).
\end{eqnarray*}
\end{example}

\section{A Procedural Semantics}
\label{procedure}

Given an action domain description $\cal D$, we use the following
procedure called CCP (Causal Completion Procedure)
to generate a complete action effect specification:
\begin{enumerate}
\item Use primitive and complex fluent definitions to generate all legal
fluent atoms. In the following
let $\cal F$ be the set of fluent atoms so generated.
\item Use action definitions to generate all legal action instances, and for each such action instance
$A$ do the following.
\begin{enumerate}
\item[2.1.] For each primitive 
fluent atom $F\in \cal F$, 
collect all ground instances\footnote{When generating ground instances, all shorthands like $\forall (x,p)$ are expanded. See the definition of fluent formulas in the last section.}
 of $A$'s positive effects:
\[
\effect(A,\var_1,F),\cdots, \effect(A,\var_n,F),
\]
all ground instances of $A$'s negative effects:
\[
\effect(A,\phi_1,\neg F),\cdots, \effect(A,\phi_m,\neg F),
\]
all ground instances of positive domain rules:
\[
\causes(\var_1',F),\cdots, \causes(\var_k',F),
\]
all ground instances of negative domain rules:
\[
\causes(\phi_1',\neg F),\cdots, \causes(\phi_l',\neg F),
\]
and 
generate the following pseudo successor state axiom;
\begin{eqnarray}
\align
succ(F)\equiv init(\var_1)\lor\cdots\lor init(\var_n)\lor
  succ(\var_1')\lor\cdots\lor succ(\var_l')\lor  \nonumber\\
\align\hspace*{2em}
 init(F)\land\neg [init(\phi_1)\lor\cdots\lor init(\phi_m)\lor \nonumber\\
\align\hspace*{6em}
  succ(\phi_1')\lor\cdots\lor succ(\phi_k')], \label{pssa1}
\end{eqnarray}
where for any fluent formula $\var$, $init(\var)$ is the formula obtained
from $\var$ by replacing every fluent atom $f$ in $\var$ by $init(f)$, and similarly
$succ(\var)$ is the formula obtained
from $\var$ by replacing every fluent atom $f$ in $\var$ by $succ(f)$.
Intuitively, $init(f)$ means that $f$ is true in the initial situation, and
$succ(f)$ that $f$ is true in the successor situation of performing
action $A$ in the initial situation.
\item[2.2.] Let $Succ$ be the set of pseudo successor state axioms,
one for each primitive fluent $F$, generated by
the last step, $Succ1$ the following set of axioms:
\[
Succ1=\{ succ(F)\equiv succ(\var)\D \defined(F,\var) \mbox{ is a complex
fluent definition}\},
\]
and $Init$ the following set of axioms:
\begin{eqnarray*}
\align
Init =
\{ \var \D \axiom(\var) \mbox{ is a domain axiom}\}\cup\\
\align\hspace*{3em}
\{ init(\var)\supset init(F)\D \causes(\var,F)\mbox{ is a domain rule}\}
\cup\\
\align\hspace*{3em}
\{ init(\var)\supset \neg init(F)\D \causes(\var,\neg F)\mbox{ is a domain rule}\}\cup\\
\align\hspace*{3em}
\{ init(F)\equiv init(\var)\D \defined(F,\var)\mbox{ is a complex fluent definition}\}\cup\\
\align\hspace*{3em}
\{ init(\phi_A)\D  \poss(A,\phi_A)\mbox{ is the precondition definition for $A$}\}.
\end{eqnarray*}
For each fluent atom $F$, if there is a formula $\Phi_F$ such that
\[
Init\cup Succ\cup Succ1\models succ(F)\equiv \Phi_F,
\]
and $\Phi_F$ does not mention propositions of the form $succ(f)$,
then output the axiom
\[
 succ(F)\equiv \Phi_F.
\]
Otherwise, the action $A$'s effect on $F$ is indeterminate. In this
case, output two axioms:
\begin{eqnarray*}
\align succ(F)\supset \alpha_F,\\
\align \beta_F\supset  succ(F),
\end{eqnarray*}
where $\alpha_F$ is a strongest formula satisfying the first implication,
and $\beta_F$ a weakest formula satisfying the second implication.
In the following, to be explicit about the action $A$ for which we are
computing its effects, we will write the axioms as $Succ_A$, $Init_A$,
and $Succ1_A$.
\end{enumerate}
\end{enumerate}

Conceptually, Step 2.1 in the above procedure is most significant.
In the next section, we 
shall prove that this step is provably correct under
a translation to the situation calculus causal theories of \citeA{Lin:causality}.
Computationally, Step 2.2 is the most expensive. We shall describe the
strategies that our system uses to implement it in
Section~\ref{experiment}.

For this procedure to work properly, the action domain description should
satisfy the following conditions.
\begin{enumerate}
\item 
We require that all fluent atoms in $Init$, $Succ$, and $Succ1$ be among those 
generated in Step 1. This would rule out cases like 
\[
\fluent(on(x,y),block(x)\land block(y)\land x\neq y)
\]
together with
$\defined(clear(x), \neg \exists (y, block)on(y,x))$, as the latter would
generate fluent atoms of the form $on(x,x)$ which are ruled out by the fluent
definition for $on$. Here one could either drop the inequality constraint
in the definition of $on$ or change the complex fluent definition into
$\defined(clear(x), \neg \exists (y, block)(on(y,x)\land x\neq y))$.
We could have built in a test in our procedure above to reject an
action domain description with incoherent fluent definitions like this.
One easy way of making sure this does not happen is
not to use inequality constraints in the definition of fluents.
\item As we mentioned above, for each action there should be exactly one
action precondition that captures exactly the conditions under
which the action is executable. When the action precondition is given
explicitly like this, one needs to be careful in writing action effect
axioms and domain rules so that no contradictory effects would be
generated. For instance, given $\poss(A, true)$, the action effect
axioms $\effect(A,true,F)$ and $\effect(A,true,\neg F)$ are clearly not
realizable simultaneously. Similarly, if $\causes(true,F)$ is given
as a domain rule, then one should not write
the effect axiom $\effect(A,true,\neg F)$. Had we not insisted that $A$ be
always executable, we could simply conclude that $A$ is not executable
when its effect axioms are in contradiction or when some of its effect
axioms contradict domain rules. It remains future work to extend
our procedure to allow for automatic generation of these implicitly given
action preconditions. For now, we shall assume that the given action
domain specification is consistent in the sense
that for each action instance $A$ generated in Step 1, the
following theory 
\begin{eqnarray*}
\align
Init\cup Succ\cup Succ1\cup
\{ init(\var)\supset \neg succ(F) \D \\
\align\hspace*{5em}
 \effect(A,\var,\neg F) \mbox{ is a ground instance of effect axiom}\}
\end{eqnarray*}
is consistent.
\item On a related point, our procedure assumes that information about
the initial
situation is given by $Init$. In particular, action effect axioms
should not entail any information about the initial situation. 
For instance, given $\causes(q,\neg p)$,
$\effect(A,true,p)$, and $\poss(A,true)$, it must be that in the
initial situation, $q$ cannot be true, for otherwise, it will persist
into the next situation, causing $p$ to be false, which contradicts
the action effect. Formally, this means that given any set $I$ of
atoms of the form $init(f)$, where $f$ is a primitive fluent atom,
if $I\cup I^-\cup Init$ is consistent,
then $I\cup I^-\cup Succ\cup Succ1$ is also consistent, where $I^-$, the
complement of $I$, is the following set:
\begin{eqnarray*}
\align \{ \neg init(f) \D init(f)\not\in I\mbox{ and}\\
\align\hspace*{2em}\mbox{$f$ is a primitive fluent atom generated by Step 1}\}
\end{eqnarray*}
Notice that for a similar reason, Reiter needed
what he called the consistency assumption in order for his completion
procedure to be sound and complete for generating successor state
axioms \cite{Reiter91}.
\end{enumerate}
While our action domain descriptions are clearly targeted at
specifying deterministic actions, some indeterminate effects can
sometimes arise from cyclic domain rules. For instance, consider the
following action domain description:
\begin{eqnarray*}
\align
\causes(p,p),\\
\align
\poss(A,true)
\end{eqnarray*}
For action $A$, $Init$ is a tautology, $Succ1$ is empty, and $Succ$
consists of the following pseudo-successor state axiom for $p$:
\[
succ(p) \equiv succ(p)\lor init(p),\]
which is equivalent to $init(p)\supset succ(p)$. So if initially $p$
is true, then after $A$ is performed, we know that $p$ will continue
to be true. But if $p$ is initially false, then after $A$ is performed,
we do not know if $p$ is true or not.

\begin{example}
Consider the blocks world description in Example~\ref{example}. The set
of fluent atoms generated by Step 1 is:
\begin{eqnarray*}
\align {\cal F}=\{ on(1,1), on(1,2),on(1,3),on(2,1), on(2,2),on(2,3),\\
\align\hspace*{3em} on(3,1),on(3,2),on(3,3),clear(1),clear(2),clear(3),\\
\align\hspace*{3em} ontable(1),ontable(2),ontable(3)\}.
\end{eqnarray*}
Step 2 generates the following action instances:
\begin{eqnarray*}
\align stack(1,2),stack(1,3),stack(2,1),stack(2,3),stack(3,1),stack(3,2),\\
\align unstack(1,2),unstack(1,3),unstack(2,1),unstack(2,3),unstack(3,1),\\
\align unstack(3,2), move(1,2,3), move(1,3,2), move(2,1,3), move(2,3,1),\\
\align move(3,1,2),
move(3,2,1)
\end{eqnarray*}
For each of these action instances, we need to 
go through Steps 2.1 and 2.2. For instance, for $stack(1,2)$,
there is only one effect axiom about $on(1,2)$:
\[
\effect(stack(1,2),true,on(1,2)),
\]
and the following causal rules about $on(1,2)$:
\begin{eqnarray*}
\align
\causes(on(1,1), \neg on(1,2)) ,\\
\align
\causes(on(1,3), \neg on(1,2)) ,\\
\align
\causes(on(2,2), \neg on(1,2)) ,\\
\align
\causes(on(3,2), \neg on(1,2)) ,\\
\align
\causes(ontable(1), \neg on(1,2)).
\end{eqnarray*}
Therefore 
Step 2.1 generates the following pseudo-successor state axiom for
$on(1,2)$:
\begin{eqnarray*}
\align
succ(on(1,2))\equiv true\lor \\
\align\hspace*{1em}
init(on(1,2))\land \neg [succ(on(1,1))\lor succ(on(1,3))\lor\\
\align\hspace*{2em}
succ(on(2,2))\lor succ(on(3,2)\lor succ(ontable(1))].
\end{eqnarray*}
We can similarly generate the following
pseudo-successor state axioms for the other primitive fluent atoms:
\begin{eqnarray*}
\align
succ(on(1,1))\equiv 
init(on(1,1))\land \neg [succ(on(1,2))\lor succ(on(1,3))\lor\\
\align\hspace*{2em}
 succ(on(2,1))\lor succ(on(3,1)\lor succ(ontable(1))],\\
\align
succ(on(1,3))\equiv
init(on(1,3))\land \neg [succ(on(1, 1)) \lor succ(on(1, 2)) \lor\\
\align\hspace*{2em}
succ(on(2, 3)) \lor succ(on(3, 3)) \lor succ(ontable(1))],\\
\align
succ(on(2,1))\equiv 
init(on(2,1))\land \neg [succ(on(1,1))\lor succ(on(3,1))\lor\\
\align\hspace*{2em}
succ(on(2,2))\lor succ(on(2,3))\lor succ(ontable(2))],\\
\align
succ(on(2,2))\equiv 
init(on(2,2))\land \neg [succ(on(1,2))\lor succ(on(1,3))\lor\\
\align\hspace*{2em}
 succ(on(2,1)\lor succ(on(2,3))\lor succ(ontable(2))],\\
\align
succ(on(2,3))\equiv 
init(on(2,3))\land \neg [succ(on(1,3))\lor succ(on(3,3))\lor\\
\align\hspace*{2em}
 succ(on(2,1)\lor succ(on(2,2))\lor succ(ontable(2))],\\
\align
succ(on(3,1))\equiv 
init(on(3,1))\land \neg [succ(on(3,2))\lor succ(on(3,3))\lor\\
\align\hspace*{2em}
 succ(on(1,1)\lor succ(on(1,3))\lor succ(ontable(1))],\\
\align
succ(on(3,2))\equiv 
init(on(3,2))\land \neg [succ(on(3,1))\lor succ(on(3,3))\lor\\
\align\hspace*{2em}
 succ(on(1,2)\lor succ(on(2,2))\lor succ(ontable(2))],\\
\align
succ(on(3,3))\equiv 
init(on(3,3))\land \neg [succ(on(3,1))\lor succ(on(3,2))\lor\\
\align\hspace*{2em}
 succ(on(1,3)\lor succ(on(2,3))\lor succ(ontable(3))],\\
\align succ(ontable(1))\equiv \\
\align\hspace*{1em} 
init(ontable(1))\land \neg 
 [succ(on(1,2))\lor succ(on(1,1))\lor succ(on(1,3))],\\
\align succ(ontable(2))\equiv \\
\align\hspace*{1em} init(ontable(2))\land \neg 
 [succ(on(2,1))\lor succ(on(2,2))\lor succ(on(2,3))],\\
\align succ(ontable(3))\equiv \\
\align\hspace*{1em} init(ontable(3))\land \neg 
 [succ(on(3,1))\lor succ(on(3,2))\lor succ(on(3,3))].
\end{eqnarray*}
For the complex fluent $clear$, its definition yields the following axioms:
\begin{eqnarray*}
\align
succ(clear(1)) \equiv \neg succ(on(1,1))\land \neg succ(on(2,1))
\land \neg succ(on(3,1)),\\
\align
succ(clear(2)) \equiv \neg succ(on(1,2))\land \neg succ(on(2,2))\land
\neg succ(on(3,2)),\\
\align
succ(clear(3)) \equiv \neg succ(on(1,3))\land \neg succ(on(2,3))\land
\neg succ(on(3,3)).
\end{eqnarray*}
We can then ``solve'' these pseudo-successor state
axioms and generate the following successor state axioms:
$$
\begin{tabular}{lll}
$succ(on(1, 1)) \equiv false$ & $succ(on(1, 2)) \equiv true$ \\
$succ(on(1, 3)) \equiv false$ &
$succ(on(2, 1)) \equiv false$ \\
$succ(on(2, 2)) \equiv false$ &
$succ(on(2, 3)) \equiv init(on(2, 3))$ \\
$succ(on(3, 1)) \equiv false$ &
$succ(on(3, 2)) \equiv false$\\
$succ(on(3, 3)) \equiv init(on(3, 3))$ &
$succ(ontable(1)) \equiv false$ \\
$succ(ontable(2)) \equiv init(ontable(2))$&
$succ(ontable(3)) \equiv init(ontable(3))$\\
$succ(clear(1)) \equiv init(clear(1))$ &
$succ(clear(2)) \equiv false$\\
$succ(clear(3)) \equiv init(clear(3))$
\end{tabular}
$$
Once we have a set of these fully instantiated successor state axioms,
we then generate STRIPS-like descriptions like the following:
\begin{verbatim}
stack(1, 2)     
Preconditions:  ontable(1), clear(1), clear(2).
Add list:       on(1, 2).
Delete list:    ontable(1), clear(2).
Cond. effects:  none.
Indet. effects: none.

stack(1, 3) 
Preconditions:  ontable(1), clear(1), clear(3).
Add list:       on(1,3).
Delete list:    ontable(1), clear(3).
Cond. effects:  none.
Indet. effects: none.
\end{verbatim}
\newpage
We have the following remarks:
\begin{itemize}
\item Although we generate the axiom $succ(on(1,3))\equiv false$
for $stack(1,2)$, we do not put $on(1,3)$ into its delete list. This
is because we can deduce $init(on(1,3))\equiv false$
from $Init$ as well.
A fluent atom is put into the add or the delete list of an action
only if this fluent atom's truth value
is definitely changed by the action. See Section~\ref{experiment} for
more details about how a STRIPS-like description is generated from successor
state axioms.
\item As one can see, our CCP procedure crucially depends on the fact
that each type has a finite domain so that all reasoning can be done
in propositional logic. This is a limitation of our
current system, and this limitation is not as bad as one might think.
First of all, typical planning problems all assume finite domains, and changing
the domain of a type in an action description is easy - all one needs to
do is to change the corresponding type definition. More significantly,
a generic action domain description can often be obtained from one
that assumes a finite domain. In our blocks world example, the numbers
``1'', ``2'', and ``3'' are generic names, and can be replaced by
parameters. For instance, if we replace ``1'' by $x$ and ``2'' by $y$
in the above STRIPS-like description of $stack(1,2)$, we will get
a STRIPS-like description for $stack(x,y)$ that works for any $x$ and $y$.
We have found that this is a strategy that often works in planning domains.
\end{itemize}
\end{example}

\section{Formal Semantics}
\label{formal-semantics}

The formal semantics of an action domain description is defined by 
translating it
into a situation calculus causal theory of \citeA{Lin:causality}.
We shall show that the procedure CCP given above is sound under this
semantics.

This section is mainly for those who are interested in nonmonotonic
action theories. For those who are interested only in using our action
description language for describing action domains, this section can
be safely skipped.

We first briefly review the language of the situation calculus.

\subsection{Situation Calculus}

The language of the situation calculus is a many sorted first-order 
language. We assume the following sorts: {\em situation} for situations,
{\em action} for actions, {\em fluent} for propositional fluents, 
{\em truth-value} for
truth values $true$ and $false$, and {\em object} for everything else.

We use the following domain independent predicates and  functions:
\begin{itemize}
\setlength{\itemsep}{0.0pt}
\item Binary function $do$ - for any action $a$ and any situation $s$,
$do(a,s)$ is the situation
resulting from performing $a$ in $s$.
\item Binary predicate $\holds$ - for any $p$ and any
situation $s$, $\holds(p,s)$ is true if $p$ holds in $s$.
\item Binary predicate $Poss$ - for any action $a$ and any situation $s$,
$Poss(a,s)$ is true if $a$ is possible (executable) in $s$.
\item Ternary predicate $Caused$ - for any fluent atom $p$, any truth value
$v$, and any situation $s$, $Caused(p,v,s)$ is true if the fluent atom $p$ is caused 
(by something unspecified) to have the truth value $v$ in the situation
$s$.
\end{itemize}

In the last section, we introduced fluent formulas. We now extend $\holds$
to these formulas: for any fluent formula $\var$ and situation $s$,
$\holds(\var,s)$ is defined as follows:
\begin{itemize}
\item $\holds(t_1=t_2,s)$ is $t_1=t_2$.
\item if $P$ is a static proposition, then $\holds(P,s)$ is $P$.
\item inductively, $\holds(\neg \var,s)$ is $\neg \holds(\var,s)$,
$\holds(\var\lor \var',s)$ is $\holds(\var,s)\lor \holds(\var',s)$,
and similarly for other connectives.
\item inductively, $\holds(\forall (x,p)\var,s)$ is
$\forall x. [p(x)\supset \holds(\var,s)]$ and
$\holds(\exists (x,p)\var,s)$ is $\exists x. [p(x)\land \holds(\var,s)]$.
\end{itemize}
According to this definition, $\holds(\var,s)$ will be expanded to a situation
calculus formula where $\holds$ is applied to fluents.

\subsection{A Translation to the Situation Calculus}

Given a first-order language $\cal L$ for writing action domain descriptions,
we assume that there will be a corresponding language ${\cal L}'$ for
the situation calculus such that constants in $\cal L$ will be constants
of sort $object$
in ${\cal L}'$, types in $\cal L$ will be types (unary predicates) in
${\cal L}'$, static relations will be predicates of the same arities in
${\cal L}'$, fluents in $\cal L$ will be functions of sort $fluent$ in
${\cal L}'$, and actions in $\cal L$ will be functions of sort $action$
in ${\cal L}'$. Under these conventions, the following translation will
map an action domain description to a situation calculus theory.

Let $\cal D$ be an action domain description. The translation of $\cal D$
into a situation calculus theory is defined as follows:
\begin{itemize}
\item a type definition $\domain(p,\{a_1,...,a_k\})$ is translated to:
\begin{eqnarray*}
&
(\forall x). p(x)\equiv (x=a_1\lor\cdots\lor x=a_k),&\\
& a_1\neq a_2\neq\cdots\neq a_k.&
\end{eqnarray*}
\item a primitive fluent definition
\[
\fluent(f(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\land\cdots
\land e_m)
\]
is translated to
\[
(\forall x_1,...,x_n).
\fluent(f(x_1,...,x_n))\equiv p_1(x_1)\land\cdots\land p_n(x_n)\land
 e_1\land\cdots\land e_m.
\]
\item a complex fluent definition
\begin{eqnarray*}
\align
\complex(f(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x)\land e_1\cdots\land e_m),\\
\align \defined(f(x_1,...,x_n), \var),
\end{eqnarray*}
is translated to
\begin{eqnarray*}
\align
(\forall x_1,...,x_n). \fluent(f(x_1,...,x_n))\equiv
 p_1(x_1)\land\cdots\land p_n(x)\land e_1\cdots\land e_m,\\
\align
(\forall x_1,...,x_n,s). \fluent(f(x_1,...,x_n))\supset
[\holds(f(x_1,...,x_n),s)\equiv \holds(\var,s)].
\end{eqnarray*}
\item a domain axiom about static propositions:
\[
\axiom(\var)
\]
is translated to $\var$ with quantifiers in it treated as shorthands:
\begin{eqnarray*}
\align
\forall (x,p)\phi = \forall x. p(x)\supset \phi,\\
\align
\exists (x,p)\phi = \exists x. p(x)\land \phi.
\end{eqnarray*}
\item an action definition
\[
\action(a(x_1,...,x_n), p_1(x_1)\land\cdots\land p_n(x_n)\land e_1\land
\cdots\land e_m)
\]
is translated to
\[
(\forall x_1,...,x_n).
\action(a(x_1,...,x_n))\equiv p_1(x_1)\land\cdots\land p_n(x_n)\land
 e_1\land\cdots\land e_m.
\]
We assume here that the domain description has only one action definition
for each action.
\item An action precondition axiom
\[
\poss(a(x_1,...,x_n), \var)
\]
is translated to 
\[
(\forall \vec{\xi},s). \action(a(x_1,...,x_n))\supset
[Poss(a(x_1,...,x_n),s)\equiv \holds(\var,s)],
\]
where $\vec{\xi}$ is the list of all free variables in $a(x_1,...,x_n)$ and
$\var$.
We mentioned earlier that one of the limitations of our current system is
that action preconditions have to be given explicitly. This is reflected
in the above translation.
\item An action effect axiom:
\[
\effect(a(x_1,...,x_n), \var, f(y_1,...,y_k)),
\]
is translated to
\begin{eqnarray*}
\align
(\forall \vec{\xi},s). \action(a(x_1,...,x_n))\land 
\fluent(f(y_1,...,y_k))\land Poss(a(x_1,...,x_n),s)
\supset\\
\align\hspace*{3em}
\{\holds(\var,s)\supset \caused(f(y_1,...,y_k),true,do(a(x_1,...,x_n),s))\},
\end{eqnarray*}
where $\vec{\xi}$ is the list of all free variables in $a(x_1,...,x_n)$,
$f(y_1,...,y_k)$,  and $\var$.

Similarly, an effect axiom 
\[
\effect(a(x_1,...,x_n), \var, \neg f(y_1,...,y_k)),
\]
is translated to
\begin{eqnarray*}
\align 
(\forall \vec{\xi},s). \action(a(x_1,...,x_n))\land 
\fluent(f(y_1,...,y_k))\land Poss(a(x_1,...,x_n),s)\supset\\
\align\hspace*{3em}
\{ \holds(\var,s)\supset \caused(f(y_1,...,y_k),false, do(a(x_1,...,x_n),s))\}.
\end{eqnarray*}
\item A domain rule of the form
\[
\causes(\var, f(x_1,...,x_n))
\]
is translated to
\[
(\forall \vec{\xi}). \fluent(f(x_1,...,x_n))\supset
(\forall s) \{ \holds(\var,s)\supset \caused(f(x_1,...,x_n),true,s)\},
\]
where $\vec{\xi}$ is the list of all free variables in $f(x_1,...,x_n)$ and
$\var$.
Similarly, a domain rule of the form
\[
\causes(\var, \neg f(x_1,...,x_n))
\]
is translated to
\[
(\forall \vec{\xi}). \fluent(f(x_1,...,x_n))\supset
(\forall s)\{ \holds(\var,s)\supset \caused(f(x_1,...,x_n),false,s)\}.
\]
\end{itemize}

Now given an action domain description $\cal D$, let $\cal T$ be its
translation in the situation calculus. The semantics of $\cal T$ is
then determined by its completion $comp({\cal T})$ that is defined as
the set of following sentences:
\begin{enumerate}
\item The circumscription of $Caused$ in $T$ with all other predicates fixed.
\item The following basic axioms about $Caused$ that says that if
a fluent atom is caused to be true (false), then it is true (false):
\begin{eqnarray}
\align Caused(p,true,s)\supset Holds(p,s),\label{causality1}\\
\align Caused(p,false,s)\supset \neg Holds(p,s).\label{causality2}
\end{eqnarray}
\item For the truth values, the following unique names and domain closure
axiom:
\begin{equation}
 true\neq false\land (\forall v) (v=true\lor v=false).
\label{truthvalue}
\end{equation}
\item 
The unique names assumptions for fluents and actions.
Specifically,
if $F_1$,..., $F_n$ are all the fluents, then we have:
\begin{eqnarray*}
\align F_i(\vec{x})\neq F_j(\vec{y}), \mbox{ $i$ and $j$ are different,}
\\[.5ex]
\align F_i(\vec{x})=F_i(\vec{y})\supset \vec{x}=\vec{y}.
% \label{unf2}
\end{eqnarray*}
Similarly for actions.
\item For each primitive fluent atom $F$, the following generic successor
state axiom:
\begin{eqnarray}
\align
\forall a,s. Poss(a,s)\supset \holds(F,do(a,s))\equiv \label{pssa2}
\\
\align\hspace*{2em}
[ \caused(F,true,do(a,s))\lor \holds(F,s)\land \neg \caused(F,false,do(a,s))].
\nonumber 
\end{eqnarray}
\item The {\em foundational axioms} \cite{LinReiter:constraint}
for the {\em discrete} situation calculus. These axioms characterize
the structure of the space of situations. For the purpose of this
paper, it is enough to mention that they include the following unique names axioms
for situations:
\begin{eqnarray*}
& s\neq do(a,s),&\\
& do(a,s)=do(a',s')\supset (a=a'\land s=s').&
\end{eqnarray*}
\end{enumerate}

The following theorem shows that the procedural semantics given in the
previous section is sound 
%and complete 
with respect to the semantics given here.

\begin{theorem}
\label{soundness}
Let $\cal D$ be an action domain description, and $\cal T$ its translation in the
situation calculus.  
Let $A$ be any ground action instance, $s$ a situation variable, and
$\var(s)$ a situation calculus
formula that satisfies the following two conditions
(1) it contains at most the two situation terms $s$ and $do(A,s)$; and
 (2) it does
not mention any predicate other than $\holds$, equality, and 
static relations.
Let $\hat{\var}$ be obtained from $\var$ by replacing each $\holds(f,s)$ in
it by $init(f)$, and each $\holds(f,do(A,s))$ in it by $succ(f)$.
Then
\begin{equation}
comp({\cal T})\models \forall s. Poss(A,s)\supset \var(s)
\label{eq:thm1}
\end{equation}
if
\begin{equation}
Init\cup Succ\cup Succ_1\models \hat{\var},
\label{eq:thm2}
\end{equation}
where $Init$, $Succ$, and $Succ_1$ are the sets of axioms generated for
$A$ according to the procedure in Section \ref{procedure}
\end{theorem}
\begin{proof}
Suppose $S$ is a situation and $M$ is a model
of $comp({\cal T})\cup \{ Poss(A,S)\}$. 
Construct
$M_{S,A}$ as follows:
\begin{itemize}
\item the domain of $M_{S,A}$ is the object domain of $M$.
\item the interpretations of non-situational function and predicate
symbols in $M_{S,A}$ are the same as those in $M$.
\item for any fluent atom $f$, $M_{S,A}\models init(f)$ iff $M\models \holds(f,S)$
and $M_{S,A}\models succ(f)$ iff $M\models \holds(f,do(A,S))$.
\end{itemize}
Clearly, 
$M\models\var(S)$ iff $M_{S,A}\models\hat{\var}$. 
We show below that
$M_{S,A}$ 
is a model of the left hand side of (\ref{eq:thm2}).
From this, we see that if
(\ref{eq:thm2}), then (\ref{eq:thm1}).

Notice first that a ground fluent atom $F$
is generated by the procedure CCP iff
$\fluent(F)$ is true in $M$. Notice also that all fluent atoms in
$Init\cup Succ\cup Succ_1$ must be generated by the procedure.

We show first that $M_{S,A}$ is a model of $Init$:
\begin{enumerate}
\item If $Axiom(\psi)$ is a domain axiom, then $\psi$ is in $\cal T$. Thus
$M$ satisfies $\psi$. Since $\psi$ has no fluent symbols in it, 
$M_{S,A}$ satisfies it too.
\item If $\causes(\psi,f(x_1,...,x_n))$ is a domain rule, then
\[
(\forall \vec{\xi}). \fluent(f(x_1,...,x_n))\supset
(\forall s)\{ \holds(\psi,s)\supset \caused(f(x_1,...,x_n),true,s)\}
\]
is in $\cal T$. Thus $M$ satisfies 
\[
(\forall \vec{\xi}). \fluent(f(x_1,...,x_n))\supset
(\forall s)\{ \holds(\psi,s)\supset \holds(f(x_1,...,x_n),s)\}.
\]
Thus if $init(\psi')\supset init(F)$ is a corresponding formula in $Init$,
where $\psi'$ and $F$ is some ground instantiation of $\psi$ and $f(x_1,...,x_n)$,
respectively, then $\fluent(F)$ must be true in $M$ (otherwise the above
formula would not be in $Init$), so $M$ satisfies
$\holds(\psi',S)\supset \holds(F,S)$. By the construction of
$M_{S,A}$, it satisfies $init(\psi')\supset init(F)$. The case
for $\causes(\psi,\neg f)$ is similar.
\item Suppose $\defined(F,\psi)$ is an instantiation of
a complex fluent definition such that $F\equiv \psi$ is in $Init$. For it
to be in $Init$, $\fluent(F)$ must be true. Thus $M$ must satisfy
$\holds(F,S)\equiv \holds(\psi,S)$. By the construction of $M_{S,A}$, it
satisfies $init(F)\equiv init(\psi,S)$.
\item Suppose $\poss(A,\phi_A)$ is the precondition axiom for $A$. Since
$M$ satisfies $Poss(A,S)$ and $\action(A)$ (because $A$ is one of the action
instances
generated by the procedure), thus $M$ satisfies $\holds(\phi_A,S)$. So
$M_{S,A}$ satisfies $init(\phi_A)$.
\end{enumerate}
We now show that $M_{S,A}$ is a model of $Succ$, that is, for each 
primitive fluent atom
$F$ generated by the procedure in Step 1, the pseudo-successor state axiom
(\ref{pssa1}) holds.
Referring to the notation in the axiom, we need to show that $M$ satisfies
the following formula:
\begin{eqnarray*}
\align
\holds(F,do(A,S))\equiv \holds(\var_1,S)\lor\cdots\lor \holds(\var_n,S)\lor\\
\align\hspace*{2em}
 \holds(\var_1',do(A,S))\lor\cdots\lor \holds(\var_l',do(A,S))\lor \\
\align\hspace*{2em}
 \holds(F,S)\land\neg [\holds(\phi_1,S)\lor\cdots\lor \holds(\phi_m,S)\lor\\
\align\hspace*{5em}
  \holds(\phi_1',do(A,S))\lor\cdots\lor \holds(\phi_k',do(A,S))].
\end{eqnarray*}
First of all, instantiating the generic successor state axiom (\ref{pssa2})
over $A$ and $S$, we get:
\begin{eqnarray*}
\align
Poss(A,S)\supset \holds(F,do(A,S))\equiv \nonumber \\
\align\hspace*{2em}
[ \caused(F,true,do(A,S))\lor \holds(F,S)\land \neg \caused(F,false,do(A,S))].
\end{eqnarray*}
Since $M$ is a model of $Poss(A,S)$, we have
\begin{eqnarray}
\align
\holds(F,do(A,S))\equiv \label{proof1} \\
\align\hspace*{2em}
[ \caused(F,true,do(A,S))\lor \holds(F,S)\land \neg \caused(F,false,do(A,S))].
\nonumber
\end{eqnarray}
Now consider the circumscription of $\caused$ in $\cal T$ with all other
predicates fixed. Notice that all axioms about $\caused$ in $\cal T$ have
the form $W\supset \caused(x,y,z)$, where $W$ is a formula that does not
mention $\caused$. Therefore the circumscription of $\caused$ is equivalent to
the predicate completion of $\caused$. 
Suppose $F$ is $f(t)$, and that all of the axioms about $\caused(f(x),v,s)$
in $\cal T$ are as follows:
\[ W_1\supset \caused(f(x),v,s),\cdots, W_i\supset \caused(f(x),v,s).\]
Because of the unique names axioms about fluents, the result of predicate
completion on $\caused$ will entail:
\[
\caused(f(x),v,s)\equiv W_1\lor\cdots\lor W_i.
\]
Now $W_1$,...,$W_i$ are from action effect axioms and domain rules about $f$.
By the way that (\ref{pssa1}) is generated, and 
noting that $\action(A)$, $\fluent(F)$, and
$Poss(A,S)$ are true, one can see that when the above equivalence is instantiated
by replacing $t$ for $x$, $true$ for $v$, and $S$ for $s$, we will get
\begin{eqnarray*}
\align
\caused(F,true,do(A,S)) \equiv
\holds(\var_1,S)\lor\cdots\lor \holds(\var_n,S)\lor\\
\align\hspace*{2em}
 \holds(\var_1',do(A,S))\lor\cdots\lor \holds(\var_l',do(A,S)).
\end{eqnarray*}
Similarly, we have the following axiom
about $\caused(F,false,do(A,S))$:
\begin{eqnarray*}
\align \caused(F,false,do(A,S)) \equiv
\holds(\phi_1,S)\lor\cdots\lor \holds(\phi_m,S)\lor\\
\align\hspace*{2em}
 \holds(\phi_1',do(A,S))\lor\cdots\lor \holds(\phi_k',do(A,S)).
\end{eqnarray*}
From these two axioms and (\ref{proof1}), we get:
\begin{eqnarray*}
\holds(F,do(A,S)) &\equiv&
\holds(\var_1,S)\lor\cdots\lor \holds(\var_n,S)\lor\\
&& \holds(\var_1',do(A,S))\lor\cdots\lor \holds(\var_l',do(A,S))\lor\\
&&
 \holds(F,S)\land \neg [
\holds(\phi_1,S)\lor\cdots\lor \holds(\phi_m,S)\lor\\
&&\hspace*{5.5em}
 \holds(\phi_1',do(A,S))\lor\cdots\lor \holds(\phi_k',do(A,S))].
\end{eqnarray*}
Since $M$ is a model of $Comp({\cal T})$, $M$ satisfies the above formula.
By the construction of $M_{S,A}$, it satisfies the pseudo-successor
state axiom (\ref{pssa1}).

Finally, the fact that $M_{S,A}$ is a model of $Succ1$ should be
apparent.
\end{proof}

In general, (\ref{eq:thm1}) does not imply (\ref{eq:thm2}). There are
several reasons:
\begin{itemize}
\item As we mentioned after the procedure CCP, we assume that
all information about the initial
situation is given by $Init$. 
\item Our procedure works on actions one at a time. The situation
calculus theory $\cal T$ captures the effects of all actions in a
single theory. So it is possible that a bad specification of an action
causes the entire theory to become inconsistent. For instance, if we
have $\causes(true, p)$, $\poss(A,true)$, and $\effect(A, false, p)$,
then the corresponding situation calculus theory will be inconsistent
because of action $A$. But for our procedure, it will generate an
inconsistent theory only on $A$.
\end{itemize}





\section{An Implementation}
\label{experiment}

Except for Step 2.2, the procedure CCP in Section~\ref{procedure} is
straightforward to implement. This section describes the strategy that
our system uses for implementing Step 2.2.
The main idea comes from the work of
\citeA{Lin:snc} on 
strongest necessary and weakest sufficient conditions.

Given a propositional theory $T$, a proposition $q$, and a set $B$ of 
propositions, a formula $\var$
is said
to be a sufficient condition of $q$ on $B$ under $T$ if 
$\var$ consists of propositions in $B$ and
$T\models \var\supset q$. It is said to be the {\em weakest} sufficient
condition if for any such sufficient condition $\var'$, we have that
$T\models \var'\supset \var$. 
Similarly, 
a formula $\var$ is said
to be a necessary condition of $q$ on $B$ under $T$ if 
$\var$ consists of propositions in $B$ and
$T\models q\supset \var$. It is said to be the {\em strongest} necessary
condition if for any such necessary condition $\var'$, we have that
$T\models \var\supset \var'$. 

It is easy to see that the weakest sufficient condition and the
strongest necessary condition are unique up to logical equivalence
under the background theory.
It was shown \cite{Lin:snc} that
these two notions are closely related, and can be computed using
the technique of forgetting \cite{LinReiter:forgetting}. In particular,
for action theories, an effective strategy is to first compute the
strongest necessary condition, add it to the background theory, and then
compute the weakest sufficient condition under the new theory. This strategy
is justified by the following proposition \citeA{Lin:snc}:
\begin{proposition}
\label{prop3}
Let $T$ be a theory, $q$ a proposition, and $B$ a set of
propositions.
If $\var$ is a necessary condition of $q$ on $B$ under $T$,
and $\psi$ the weakest sufficient condition of $q$ on $B$ under
 $T\cup \{\var\}$, 
then $\var\land\psi$ is the
weakest sufficient condition of $q$ on $B$ under $T$.
\end{proposition}

We can now describe our strategy for implementing Step 2.2 of 
the procedure CCP. In the following,
given an action instance $A$,
as in Step 2.2,
let $Succ$ be the set of pseudo-successor state axioms for
primitive fluent atoms, $Succ1$ the set of pseudo-successor state axioms
for complex fluent atoms, and
$Init$ the set of initial
situation axioms derived from the action precondition axiom for $A$,
domain axioms, domain rules, and complex fluent definitions.
Also in the following, a $succ$-proposition is one of the form $succ(f)$,
and an $init$-proposition is one of the form $init(f)$.
\begin{enumerate}
\item Transform $Init$ into a clausal form and derive
from it a set of unit clauses $Unit$.
\item Use $Unit$ to simplify the axioms in $Succ$ and for each resulting
axiom in it:
\begin{equation}
\label{succ}
succ(f)\equiv \Phi_f,
\end{equation}
if $\Phi_f$ does not mention $succ$-propositions, then delete it
from $Succ$, output it and
replace $succ(f)$ in the rest of the axioms by $\Phi_f$.
\item For each fluent atom $f$ whose pseudo-successor state axiom
(\ref{succ}) is in $Succ$, if $\Phi_f$ has
the form $init(f)\land ...$ (a candidate of a frame axiom), then
check to see if $succ(f)$ can be derived from $Succ$, $Unit$, and
$init(f)$ by unit resolution. If so, delete it from $Succ$, output
$succ(f)\equiv init(f)$, and replace $succ(f)$ in $Succ$ by $init(f)$.
\item  For each fluent atom $f$ whose pseudo-successor state axiom
(\ref{succ}) is in $Succ$,
compute the strongest necessary condition $\alpha_f$ of $succ(f)$ on the
$init$-propositions under the theory $Init\cup Succ$, and
the weakest sufficient condition $\beta_f$ of
$succ(f)$ on the $init$-propositions under the theory
$\{ \alpha_f\}\cup Init\cup Succ$. If $\beta_f$ is a tautology,
then delete (\ref{succ}) from $Succ$, output $succ(f)\equiv \alpha_f$,
and replace $succ(f)$ in $Succ$ by $\alpha_f$. If $\beta$ is not
a tautology, then output $succ(f)\supset\alpha_f$ and
$\alpha_f\land\beta_f\supset succ(f)$, but do not delete (\ref{succ}) from
$Succ$. The correctness of this step follows from Proposition~\ref{prop3}.
\item The previous steps solve the equations in $Succ$, and generate
appropriate output for primitive fluent atoms. For each complex fluent atom $F$:
\[
\defined(F, \var),
\]
if every primitive fluent atom in $\var$ has a successor state axiom, then
do the following:
\begin{enumerate}
\item if no primitive fluent atoms in $\var$ are changed by the action, then
this complex fluent atom is not changed by the action either, so
output $succ(F)\equiv init(F)$;
\item otherwise, output $succ(F)\equiv \Phi$, where $\Phi$ is obtained from
$succ(\var)$ by replacing every $succ$-proposition in it by the right
side of its successor state axiom.
\end{enumerate}
Otherwise, if some of the primitive fluent atoms in $\var$ do not have a successor
state axiom, which means the action may have an indeterminate effect on them,
then this action may have an indeterminate effect on $F$ as well. Compute
the strongest necessary and weakest sufficient conditions of $succ(F)$
under $Init\cup Succ\cup Succ1$ as in the last step, and output them.
\item This step will try to generate a STRIPS-like description for the
action instance $A$ based on the results of Steps 4 and 5. For each
fluent atom $F$, do according to one of the following cases:
\begin{enumerate}
\item if its successor state axiom is $succ(F)\equiv true$, then
put $F$ into the add list unless $init(F)$ is entailed by $Init$;
\item if its successor state axiom is $succ(F)\equiv false$, then
put $F$ into the delete list unless $\neg init(F)$ is entailed by $Init$;
\item if its successor state axiom is $succ(F)\equiv \Phi$, and $\Phi$ is
not the same as $true$, $false$, or $init(F)$, then put $F$ in the 
conditional effect list and output its successor
state axiom.
\item If $F$ does not have a successor state axiom, then put it in the list
of indeterminate effects.
\end{enumerate}
Clearly, if $F$ is not put into any of the lists, then its truth value is
not affected by $A$.
\end{enumerate}
Steps 4 and 5  of 
the above procedure are the bottleneck as
in the worst case,
computing the strongest necessary condition of a proposition is coNP-hard.
However, it has been our experience that if action $A$ has a context-free
effect on fluent atom $F$, then its successor state axiom can be computed
without going through Step 4.

We have implemented the procedure CCP using the above strategy
in SWI-Prolog 3.2.9\footnote{SWI-Prolog is developed by
Jan Wielemaker at University of Amsterdam}. The url for this system
is as follows:
\begin{verbatim}
http://www.cs.ust.hk/~flin/ccp.html
\end{verbatim}
Using the system, we have encoded in our action description language
many of the planning domains
that come with the original release of PDDL \cite{McDermott:PDDL}, and
compiled them to STRIPS-like specifications. Our encodings of the domains
and the results returned by the system are 
included in the online appendix. In the following, we illustrate
some interesting features of our system using the following two domains:
the blocks world and the monkey and bananas domain.


%\section{Some Experimental Results}

\subsection{The Blocks World}

We have used the blocks world as the running example. Here we shall
give an alternative specification of the domain using the following
better known set of actions: $stack$, $unstack$, $pickup$, and
$putdown$. We shall use this domain to
show that changing
slightly the precondition of one of the actions can result in a very 
different action specification.

We begin with a description that corresponds to the standard STRIPS
encoding of the domain.
\begin{eqnarray*}
\align
\fluent(on(x,y), block(x)\land block(y)),\\
\align
\fluent(ontable(x), block(x)),\\
\align
\fluent(holding(x), block(x)),\\
\align
\complex(clear(x), block(x),\\
\align
\defined(clear(x), (\neg \exists(y,block) on(y,x)) \land \neg holding(x)),\\
\align
\complex(handempty, true),
\\
\align
\defined(handempty, \neg\exists(x, block)holding(x)),\\[1ex]
\align
\causes(on(x,y)\land x\neq z, \neg on(z,y)),\\
\align
\causes(on(x,y)\land y\neq z, \neg on(x,z)),\\
\align
\causes(on(x,y), \neg ontable(x)),\\
\align
\causes(ontable(x), \neg on(x,y)),\\
\align
\causes(on(x,y), \neg holding(x)),\\
\align
\causes(on(x,y), \neg holding(y)),\\
\align
\causes(holding(x), \neg ontable(x)),\\
\align
\causes(holding(x), \neg on(x,y)),\\
\align
\causes(holding(x), \neg on(y,x)),\\
\align
\causes(holding(x)\land y\neq x, \neg holding(y)),\\[1ex]
\align
\action(stack(x,y), block(x)\land block(y)\land x\neq y),\\
\align
\poss(stack(x,y),holding(x)\land clear(y)),\\
\align
\effect(stack(x,y),true,on(x,y)),\\[1ex]
\align
\action(unstack(x,y), block(x)\land block(y)\land x\neq y),\\
\align
\poss(unstack(x,y),clear(x)\land on(x,y)\land handempty),\\
\align
\effect(unstack(x,y),true,holding(x)),\\[1ex]
\align
\action(putdown(x), block(x)),\\
\align
\poss(putdown(x),holding(x)),\\
\align
\effect(putdown(x),true,ontable(x)),\\[1ex]
\align
\action(pickup(x), block(x)),\\
\align
\poss(pickup(x), handempty\land ontable(x)\land clear(x)),\\
\align
\effect(pickup(x), true, holding(x)).
\end{eqnarray*}
Notice that compared to the description in Example 1, there are two
more fluents, $holding$ and $handempty$ here. Thus we have a few more
domain rules about them, and the definition of $clear$ is
changed to take into account that when a block is held, it is not 
considered to be clear.

Now assuming a domain with three blocks $\domain(block,\{1,2,3\})$,
our system will generate 19 fluent atoms, and 18 action instances.
For each action instance, it returns both a complete set of
successor state axioms and a STRIPS-like representation. 
The total computation time for all actions is
835K inferences and 0.5
seconds.\footnote{All times in this paper refer to CPU times
on a Pentium III 1GHz machine with 512MB RAM running SWI-Prolog 3.2.9 
under Linux. The number of
inferences is the one reported by SWI-Prolog, and roughly corresponds to
the number of resolution steps carried out by the Prolog interpreter, and is
machine independent.}
This is a pure STRIPS domain, i.e. all actions are context free. For this
type of domains, as we mentioned earlier,
Step 4 in our implementation procedure is not needed, and Step 5 is easy.


The results are as expected. For instance, for action $pickup(1)$, the
STRIPS-like representation returned by the system looks like the
following:
track $1$ to track $2$), the STRIPS-like representation looks like:
{\tt
\begin{verbatim}
pickup(1):
  Preconditions: clear(1), handempty, ontable(1)
  Add list: holding(1)
  Delete list: ontable(1), clear(1), handempty
  Conditional effects:
  Indeterminate effects:
\end{verbatim}
}
The complete output is given in the online appendix.
Now let us consider what happen if we drop $ontable(x)$ from
the precondition of $pickup(x)$:
\[
\poss(pickup(x), handempty\land clear(x)).
\]
This means that as long as a block is clear, it can be picked up.
With this new precondition, our system returns the following
STRIPS-like representation
for action $pickup(1)$;
{\tt
\begin{verbatim}
pickup(1):
  Preconditions: clear(1), handempty
  Add list: holding(1)
  Delete list: clear(1), handempty, on(1, 2), on(1, 3), ontable(1)
  Conditional effects:
     succ(clear(2))<-> - (init(on(2, 2))\/init(on(3, 2)))
     succ(clear(3))<-> - (init(on(2, 3))\/init(on(3, 3)))
  Indeterminate effects: 
\end{verbatim}
}
Here ``\verb+-+'' is negation, and ``\verb-\/-'' is disjunction.
An ADL-like description for this action would be something like the
following:
{\tt
\begin{verbatim}
pickup(x):
  Preconditions: clear(x), handempty
  Add list: holding(x),
            clear(y) when on(x,y)
  Delete list: clear(x), handempty, 
               on(x,y) when on(x,y)
               ontable(x) when ontable(x)
\end{verbatim}
}

\subsection{The Monkey and Bananas Domain}

This domain is again adapted from McDermott's PDDL library of planning
domains, which attributes it to 
the University of Washington's UCPOP collection of action domains, which
in turn attributes it to Prodigy.
While some of the action effects generated by our system are
context-dependent, they are all context-free in the other systems.
We shall elaborate on this difference later.

In this domain, there are two types, $loc$ for locations (we assume
there are three locations here), and
$object$ for things like monkey, banana, box, etc.:
\begin{eqnarray*}
\align \domain(loc, \{ 1,2,3\}),\\
\align \domain(object, \{ monkey, box,banana,knife,glass,fountain\}).
\end{eqnarray*}
The following are fluent definitions:
\begin{eqnarray*}
\align
\fluent(onFloor),\\
\align
\fluent(at(M,X), object(M)\land loc(X)),\\
\align
\fluent(hasknife),\\
\align
\fluent(onbox(X), loc(X)),\\
\align
\fluent(hasbanana),\\
\align
\fluent(haswater),\\
\align
\fluent(hasglass).
\end{eqnarray*}
The following are domain rules about these fluents:
\begin{eqnarray}
\align
\causes(onbox(X),at(monkey,X)),\\
\align
\causes(onbox(X), at(box,X)),\\
\align
\causes(onbox(X), \neg onFloor),\\
\align
\causes(onFloor, \neg onbox(X)),\\
\align
\causes(at(M,X)\land X\neq Y, \neg at(M,Y)),\\
\align
\causes(hasglass \land at(monkey, X), at(glass,X)), \label{monkey1}\\
\align
\causes(hasknife \land at(monkey, X), at(knife,X)),\\
\align
\causes(hasbanana \land at(monkey, X), at(banana,X)) \label{monkey2}.
\end{eqnarray}

The following are action definitions along with their respective
preconditions and effect axioms:
\begin{itemize}
\item $goto(x,y)$ - the monkey goes to $x$ from $y$:
\begin{eqnarray*}
\align
\action(goto(X,Y), loc(X)\land loc(Y)\land X\neq Y),\\
\align
\poss(goto(X,Y), at(monkey,Y)\land onFloor),\\
\align
\effect(goto(X,Y), true, at(monkey,X)).
\end{eqnarray*}
\item $climb(X)$ -  the monkey climbs onto the box at location $X$:
\begin{eqnarray*}
\align
\action(climb(X), loc(X)),\\
\align
\poss(climb(X), at(box,X)\land onFloor\land at(monkey, X)),\\
\align
\effect(climb(X), true, onbox(X)).
\end{eqnarray*}
\item $pushbox(X,Y)$ -  the monkey pushes the box from $Y$ to $X$.
\begin{eqnarray*}
\align
\action(pushbox(X,Y), loc(X)\land loc(Y)\land X\neq Y),\\
\align
\poss(pushbox(X,Y), at(monkey,Y)\land at(box,Y))\land onFloor),\\
\align
\effect(pushbox(X,Y), true, at(monkey,X)),\\
\align
\effect(pushbox(X,Y), true, at(box,X)).
\end{eqnarray*}
\item $getknife(X)$ - get knife at location $X$.
\begin{eqnarray*}
\align
\action(getknife(X), loc(X)),\\
\align
\poss(getknife(X), at(knife,X)\land at(monkey,X)\land \neg hasknife),\\
\align
\effect(getknife(X), true, hasknife).
\end{eqnarray*}
\item $getbanana(X)$ - grab banana at loc $X$, provided the monkey is on the box.
\begin{eqnarray*}
\align 
\action(getbanana(X), loc(X)),\\
\align 
\poss(getbanana(X), onbox(X)\land at(banana,X)\land \neg hasbanana),\\
\align
\effect(getbanana(X), true, hasbanana).
\end{eqnarray*}
\item $pickglass(X)$ -  pick up glass at loc $X$.
\begin{eqnarray*}
\align
\action(pickglass(X), loc(X)),\\
\align
\poss(pickglass(X), at(glass,X)\land at(monkey,X)\land \neg hasglass),\\
\align
\effect(pickglass(X), true, hasglass).
\end{eqnarray*}
\item $getwater(X)$ - get water from fountain at loc $X$,
provided the monkey is on the box, and has a glass in hand.
\begin{eqnarray*}
\align
\action(getwater(X), loc(X)),\\
\align
\poss(getwater(X), at(fountain,X)\land onbox(X)\land hasglass\land \neg haswater),\\
\align
\effect(getwater(X), true, haswater).
\end{eqnarray*}
\end{itemize}

This domain has 27 actions and 26 fluent atoms. 
Again, for each action, our system generates both a complete set of
fully instantiated successor state axioms and a STRIPS-like representation.
For instance, for action $goto(1,2)$, the following
is the STRIPS-like representation generated by the system:
{\tt
\begin{verbatim}
Action goto(1, 2)

Preconditions: at(monkey, 2), onFloor

Add list: at(monkey, 1)

Delete list: at(monkey, 2)

Conditional effects:

succ(at(banana, 1)) <-> init(hasbanana) \/ init(at(banana, 1))
succ(at(knife, 1)) <-> init(hasknife) \/ init(at(knife, 1))
succ(at(glass, 1)) <-> init(hasglass) \/ init(at(glass, 1))
succ(at(banana, 2)) <-> - init(hasbanana) & init(at(banana, 2))
succ(at(knife, 2)) <-> - init(hasknife) & init(at(knife, 2))
succ(at(glass, 2)) <-> - init(hasglass) & init(at(glass, 2))
\end{verbatim}
}
The total running time for all actions is
8 seconds while performing 20 million inferences. About 90 percent of
time is spent on Step 4, i.e. on
computing the strongest necessary and weakest sufficient
conditions of fluent atoms on which the given action has context-dependent
effects. For instance, for action $goto(1,2)$ above,
the majority of time was spent on generating the above
6 conditional effects.

For this action, actually for all the actions in this domain, we could
use an ADL-like description \cite{Pednault89} for conditional effects:
{\tt
\begin{verbatim}
Add list: at(banana,1) when hasbanana
          at(knife,1) when hasknife
          at(glass,1) when hasglass

Delete list: at(banana,2) when hasbanana
             at(knife,2) when hasknife
             at(glass,2) when hasglass
\end{verbatim}
}
However, it is not clear whether this can always be done in the general case.


We mentioned earlier that the specifications for this domain given in
McDermott's collection as well as others are all context-free.
For instance, the following is a specification for action $goto$ in
PDDL in McDermott's collection:
\begin{verbatim}
  (:action GO-TO
             :parameters (?x ?y)
             :precondition (and (location ?x) (location ?y) 
                     (not (= ?y ?x)) (on-floor) (at monkey ?y))
             :effect (and (at monkey ?x) (not (at monkey ?y))))
\end{verbatim}
This corresponds to a context-free action that does not change any other
fluent except $at$. It is clear that the design of this
action does not take into account domain rules
(\ref{monkey1}) - (\ref{monkey2}). With this specification, if initially
banana is at location 1, then the goal of having banana at location 2
would not be achievable.

\subsection{Summary}

The other domains that we have experimented including
a scheduling domain that includes Pednault's
dictionary and paycheck domain as a special case,
the rocket domain, the SRI robot domain,
the machine shop assembling domain, the ferry domain, the grid domain,
the sokoban domain, and the gear domain. 
They are all included in the online appendix.
We summarize below some of the common features of these domains:
\begin{itemize}
\item In all the domains that we tried, it is quite straightforward
to decide what effects of an action should be encoded as
direct effects (those given by the predicate $\effect$) and what effects as
indirect effects (those derived from domain rules).
\item The most common domain rules are functional dependency constraints.
For instance, in the blocks world, the fluent atom $on(x,y)$ is functional
on both arguments; in the monkey and banana domain, the fluent atom $at(object,loc)$
is functional on the second argument (each object can be at only one location).
It makes sense then that we would have a special shorthand for 
these domain rules, and perhaps a special procedure for handling them as well.
But more significantly, given the prevalence of these functional dependency
constraints in action domains, it is worthwhile to investigate the
possibility of a general purpose planner making good use of these
constraints.
\item As we mentioned earlier, our system is propositional. The generated
successor state axioms and
STRIPS-like systems are all fully instantiated. However, it is often
easy for the user to generalize
these propositional specifications to first-order ones. 
We shall investigate the generality of this observation next.
%In this
%sense, it's best to regard this system as a semi-automatic generator of
%action domain specifications.
\end{itemize}


\section{Generalizing Propositional STRIPS-Like Systems to Ones With
Parameters}
\label{generalize}

As we mentioned, for many action
domain descriptions, the successor
state axioms and STRIPS-like systems generated for a specific domain
can be generalized to arbitrary ones. 

More precisely, let $\cal D$ be a domain description, and
\[
\domain(p_1,D_{p_1}), \cdots,\domain(p_k,D_{p_k})\]
its type specification. Suppose in $\cal D$ for action
$A$ we have that $Init_A\cup Succ_A\models \var$. Now suppose ${\cal D}'$
is another domain description that is just like $\cal D$ except that
it has a different type specification:
\[
\domain(p_1,D_{p_1}'), \cdots,\domain(p_k,D_{p_k}').\]
The question that we are interested in is this:
given any one-to-one mapping from the type
specification of $\cal D$ to that of  ${\cal D}'$, will
$Init_{A'}\cup Succ_{A'}\models \var'$ be true in ${\cal D}'$? Here $A'$
(resp. $\var'$) is
the result of replacing all objects in $A$ (resp. $\var$)
according to the mapping.

For instance, if the above is true for the blocks world, then we can
generalize the results for
the domain description in Example~\ref{example} as follows. As we have
shown, for action $stack(1,2)$, both $succ(on(1,2))$ and $\neg
succ(on(1,3))$ are true. Now if we change the type specification to
$\domain(block, \{ a,b,c,d,e\})$, and if we map $1$ to $a$, $2$ to
$c$, and $3$ to $e$, in the new domain specification, we will have
that for action $stack(a,c)$, $succ(on(a,c))$ and $\neg succ(on(a,e))$
are true. Furthermore, by changing the mapping for $3$, we see that
for any $x$ that is different from $a$ and $c$ (the mapping
needs to be one-to-one), $\neg succ(on(a,x))$ is true.

Obviously, this is to be expected of the blocks world. We
now proceed to show that for some general classes of domain
descriptions, we can do this as well.
We first make precise the mapping from one type specification to another.

\begin{definition}
Given two type specifications $O$:
\[
\domain(p_1,D_{p_1}),\cdots, \domain(p_k,D_{p_k}),
\]
and $O'$:
\[
\domain(p_1,D_{p_1}'),\cdots, \domain(p_k,D_{p_k}'),
\]
an {\em embedding} from $O$ to $O'$ is a one-to-one mapping $\tau$ from
$D_{p_1}\cup\cdots\cup D_{p_k}$ to 
$D_{p_1}'\cup\cdots\cup D_{p_k}'$ such that for any $1\leq i\leq k$,
and any $a\in D_{p_i}$, $f(a)\in D_{p_i}'$.
\end{definition}
Clearly, if there is an embedding of $O$ to $O'$, then for each type
$p$, the size of the 
domain for $p$ in $O'$ must be at least the size of the domain for $p$
in $O$. Given such an embedding $\tau$, any expression $\beta$ (actions,
propositions, formulas) in an action domain description $\cal D$ with
$O$ as its type specification
can be mapped to $\tau(\beta)$ in the language of ${\cal D}'$: one simply replaces
each object $a$ in $\beta$ by $\tau(a)$, where ${\cal D}'$ differs from
$\cal D$ only in that it uses $O'$ as its type specification. Notice
that only objects (those in the domain of some type) are to be
replaced, not constants that may occur in the effect axioms or domain rules.

\begin{definition}
An action domain description belongs to {\em simple-I} class if it
does not mention any function of positive arity, 
does not mention any complex fluents except in
complex fluent definitions, 
and 
satisfies the following conditions:
\begin{enumerate}
\item If $\poss(A,\phi_A)$ is an action precondition definition, then
  $\phi_A$ has the form\\
 $(\forall x,p)...(\forall y,q)W$, where $W$ is
  a fluent formula that does not have any quantifiers.
\item If $\effect(A,\var,F)$ or $\effect(A,\var,\neg F)$ is an action
  effect axiom, then $\var$ does not have any quantifiers, and the
  variables
 in $\var$ and $F$ are among those
  in $A$. That is, one cannot have something like
  $$\effect(explodeAt(x), nearby(y,x), dead(y)).$$
\item If $\causes(\var,F)$ or $\causes(\var,\neg F)$
 is a domain rule, then $\var$ does not have any quantifiers, and
 all the variables in
$\var$ must be in $F$.
\end{enumerate}
\end{definition}

\begin{theorem}
Let $\cal D$ be a simple-I  action domain description, 
and $A$ an action instance in $\cal D$. 
Let ${\cal D}'$ be
just like $\cal D$ except for the type specification.
Then for any formula
$\psi$ that does not
mention any complex fluent and has no quantifiers, and any embedding $\tau$
from the type specification of $\cal D$ to that of ${\cal D}'$, we
have that if 
$Init_A\cup Succ_A\models\psi$ in $\cal D$. 
then
$Init_{\tau(A)}\cup Succ_{\tau(A)}\models \tau(\psi)$ in ${\cal D}'$.
\end{theorem}
\begin{proof}
Suppose $Init_{\tau(A)}\cup Succ_{\tau(A)}\models \tau(\psi)$ is not true, and that
$M_1$ is a truth assignment in the language of ${\cal D}'$ that satisfies
$Init_{\tau(A)}\cup Succ_{\tau(A)}$ and $\neg \tau(\psi)$. Now construct a truth
assignment $M_2$ in the language of $\cal D$ as follows: for any
proposition $P$ in the language of $\cal D$ that does not mention any
complex fluent, $M_2\models P$ iff $M_1\models \tau(P)$
($P$ is really either a static
proposition, $succ(F)$,or $init(F)$, where $F$ is a primitive
fluent atom). 
The truth
values of complex fluent atoms in $M_2$ are defined according to their
definitions. Clearly, $M_2\models \psi$. We now need to show that
$M_2$ also satisfies $Init_A$ and $Succ_A$. For $Init_A$, there are
three cases:
\begin{enumerate}
\item $M_2\models init(F)\equiv init(\var)$ when $\defined(F,\var)$ is
  a complex fluent definition. This follows from the construction of $M_2$.
\item $M_2\models init(\phi_A)$ when $\poss(A,\phi_A)$ is the
  precondition definition for $A$. By our assumption, $\phi_A$ has the
  form $(\forall x,p)...(\forall y,q).W$, where $W$ is a formula
  without any quantifiers. Without loss of generality, let us assume
  it is $(\forall x, p)W$. Then this formula is equivalent to 
\[
\bigvee_{a\in D_{p}} W(x/a)
\]
under $\cal D$, where $D_{p}$ is the domain of type $p$ in $\cal D$. 
So $M_2\models (\forall x, p)W$ iff
\[
M_2\models \bigvee_{a\in D_{p}} W(x/a)
\]
iff
\[
M_1\models \bigvee_{a\in D_{p}} W(x/\tau(a)),
\]
which is true since $M_1\models (\forall x,p)W$.
\item All other formulas in $Init_A$ do not mention complex
  fluents and have no quantifiers. 
They are true in $M_2$ because the corresponding ones are
  true in $M_1$.
\end{enumerate}
For $Succ_A$, suppose $F$ is a primitive fluent atom, and its
pseudo-successor state axiom $\Phi_F$ as constructed according to the procedure
CCP given in Section~\ref{procedure} is as follows:
\begin{eqnarray*}
\align
succ(F)\equiv init(\var_1)\lor\cdots\lor init(\var_n)\lor
  succ(\var_1')\lor\cdots\lor succ(\var_l')\lor\\
\align\hspace*{2em}
 init(F)\land\neg [init(\phi_1)\lor\cdots\lor init(\phi_m)\lor
  succ(\phi_1')\lor\cdots\lor succ(\phi_k')].
\end{eqnarray*}
Because of the following properties about $\cal D$:
\begin{itemize}
\item each effect axiom $\effect(A,\var,F)$ or $\effect(A,\var,\neg F)$
has the property that $\var$ has no quantifier, and that 
the variables in $\var$ are also in $F$;
\item
each domain rule of the form $\causes(\var,F)$ or $\causes(\var,\neg F)$ has the
property that $\var$ has no quantifier, and that the variables in $\var$ are also in $F$;
\end{itemize}
 so the
pseudo-successor state axiom for $\tau(succ(F))$ under ${\cal D}'$ is
just $\tau(\Phi_F)$.
Thus $M_2\models \Phi_F$ since $M_1\models \tau(\Phi_F)$. This proves
that $M_2$ is a model of $Succ_A$, thus the theorem.
\end{proof}

However, most of the examples that we have in the paper do not belong
to this simple-I class, for two reasons: action preconditions, like
those in the blocks world, can mention complex fluents; and some of
the negative domain rules $\causes(\var,\neg F)$ may have some
variables not in $F$. The first problem is not a problem in principle as complex
fluents can be replaced by their definitions. The second problem is
more serious, and that leads to a new type of simple action theories.

\begin{definition}
An action domain description belongs to {\em simple-II} class if it
does not mention any function of positive arity, 
does not mention any complex fluents except in
complex fluent definitions, 
and 
satisfies the following conditions:
\begin{enumerate}
\item If $\poss(A,\phi_A)$ is an action precondition definition, then
  $\phi_A$ has the form\\
$(\forall x,p)...(\forall y,q)W$, where $W$ is
  a fluent formula that does not have any quantifiers.
\item If $\effect(A,\var,F)$ or $\effect(A,\var,\neg F)$ is an action
  effect axiom, then $\var$ does not have any quantifiers, and the
  variables
 in $\var$ and $F$ are among those
  in $A$.
\item There are no positive domain rules of the form $\causes(\var,F)$.
\item If $\causes(\var,\neg F)$ is a domain rule, then $\var$ must be
  of the form $\var_1\land\var_2$, where $\var_1$ is any formula
that does not mention any  fluents 
and $\var_2$ is a fluent atom. 
Notice that there is no restriction on variables in $\var_2$.
\end{enumerate}
\end{definition}

Simple-II class action domain descriptions seem to be very limited in
that there can be no positive domain rules, and the only negative
domain rules allowed are binary. Nevertheless, they still capture many
context-free action domains. For instance, both the blocks world and
meet-and-pass domains in this paper belong to this class: for the
blocks world, notice that while it uses the complex fluent
$clear$ in some of its action precondition definitions, as in 
$\poss(stack(x,y), ontable(x)\land clear(x)\land clear(y))$,
these definitions can be reformulated as follows using $clear$'s definition:
\begin{eqnarray*}
\align
\poss(stack(x,y), \\
\align\hspace*{4em}
ontable(x)\land 
(\forall x_1,block)(\forall
y_1,block)(\neg on(x_1,x)\land \neg on(y_1,y))).
\end{eqnarray*}
This will then satisfy the condition about $\poss$ in the above definition of
simple-II action domain descriptions.
While we have not verified it formally, it seems that
all the context-free action domains in McDermott's PDDL
library of action domains, including the logistics domain, belong to the
simple-II class.

\begin{theorem}
Let $\cal D$ be a simple-II action domain description,
and $A$ an action instance in $\cal D$. Let ${\cal D}'$ be just like $\cal D$
except for the type specification. Then for any
formula $\psi$ that does not
mention any complex fluent and has no quantifiers, and any embedding $\tau$ from the type specification of $\cal D$ to that of $\cal D'$, we have that if
$Init_A\cup Succ_A\models\psi$ in $\cal D$ then
$Init_{\tau(A)}\cup Succ_{\tau(A)}\models \tau(\psi)$ in $\cal D'$.
\end{theorem}
\begin{proof}
Suppose $Init_{\tau(A)}\cup Succ_{\tau(A)}\models \tau(\psi)$ is not true, and that
$M_1$ is a truth assignment in the language of ${\cal D}'$ that satisfies
$Init_{\tau(A)}\cup Succ_{\tau(A)}$ and $\neg \tau(\psi)$. Now construct a truth
assignment $M_2$ in the language of $\cal D$ as follows: for any
proposition $P$ in the language of $\cal D$ that does not mention any
complex fluent, $M_2\models P$ iff $M_1\models \tau(P)$
($P$ is really either a static
proposition, $succ(F)$,or $init(F)$, where $F$ is a primitive
fluent atom). 
The truth
values of complex fluent atoms in $M_2$ are defined according to their
definitions. Clearly, $M_2\models \psi$. We now need to show that
$M_2$ also satisfies $Init_A$ and $Succ_A$. For $Init_A$, there are
three cases:
\begin{enumerate}
\item $M_2\models init(F)\equiv init(\var)$ when $\defined(F,\var)$ is
  a complex fluent definition. This follows from the construction of $M_2$.
\item $M_2\models init(\phi_A)$ when $\poss(A,\phi_A)$ is the
  precondition definition for $A$. By our assumption, $\phi_A$ has the
  form $(\forall x,p)...(\forall y,q).W$, where $W$ is a formula
  without any quantifiers. Without loss of generality, let us assume
  it is $(\forall x, p_1)W$. Then this formula is equivalent to 
\[
W(x/a_{11})\lor\cdots\lor W(x/a_{1n_1})
\]
under $\cal D$. So $M_2\models (\forall x, p_1)W$ iff
\[
M_2\models W(x/a_{11})\lor\cdots\lor W(x/a_{1n_1})
\]
iff
\[
M_1\models W(x/\tau(a_{11}))\lor\cdots\lor W(x/\tau(a_{1n_1})),
\]
which is true since $M_1\models (\forall x,p_1)W$.
\item All other formulas in $Init_A$ do not mention complex
  fluents and have no quantifiers. 
They are true in $M_2$ because the corresponding ones are
  true in $M_1$.
\end{enumerate}
For $Succ_A$, suppose $F$ is a primitive fluent atom. Since there is no positive
domain rule of the form $\causes(\var,F)$, the
pseudo-successor state axiom for $F$ as constructed according to the procedure
CCP given in Section~\ref{procedure} must be of the following form:
\begin{eqnarray*}
\align
succ(F)\equiv init(\var_1)\lor\cdots\lor init(\var_n)\lor\\
\align\hspace*{2em}
 init(F)\land \neg [init(\phi_1)\lor\cdots\lor init(\phi_m)\lor
  succ(\phi_1')\lor\cdots\lor succ(\phi_k')],
\end{eqnarray*}
where for each $1\leq i\leq k$, $\causes(\phi_i',\neg F)$ is an
instance of a domain rule in $\cal D$.

Because in $\cal D$ and ${\cal D}'$,
each effect axiom $\effect(\var,F)$ or $\effect(\var,\neg F)$
has the property that $\var$ has no quantifier, and that 
the variables in $\var$ are also in $F$,
the
pseudo-successor state axiom for $\tau(succ(F))$ under ${\cal D}'$ must have the
form:
\begin{eqnarray}
\align 
succ(\tau(F))\equiv init(\tau(\var_1))\lor\cdots\lor init(\tau(\var_n))\lor \nonumber
\\
\align\hspace*{2em} 
 init(\tau(F))\land\neg [init(\tau(\phi_1))\lor\cdots\lor init(\tau(\phi_m))\lor \label{eq2}\\
\align\hspace*{2em} 
succ(\tau(\phi_1'))\lor\cdots\lor succ(\tau(\phi_k'))\lor succ(\phi)],
\nonumber
\end{eqnarray}
where $\phi$ is a disjunction such that each disjunct $\alpha$ must be
such that $\causes(\alpha,\neg \tau(F))$ is an instance in ${\cal D}'$
and that the fluent atom in $\alpha$ contains an object not in
$\tau(A)$ and $\tau(F)$.

There are two cases:
\begin{itemize}
\item Suppose $M_2\models succ(F)$. Then $M_1\models
succ(\tau(F))$. Since $M_1$ is a model of $Succ_{\tau(A)}$, $M_1$
satisfies the above axiom about $succ(\tau(F))$. Therefore $M_1$
satisfies the following formula:
\begin{eqnarray*}
\align 
 init(\tau(\var_1))\lor\cdots\lor init(\tau(\var_n))\lor\\
\align\hspace*{2em}
 init(\tau(F))\land\neg [init(\tau(\phi_1))\lor\cdots\lor init(\tau(\phi_m))\lor\\
\align\hspace*{8em}
  succ(\tau(\phi_1'))\lor\cdots\lor succ(\tau(\phi_k'))].
\end{eqnarray*}
Since the above formula does not mention any complex fluents and has
no quantifiers, $M_2$
satisfies the corresponding formula:
\begin{eqnarray}
\align \label{eq1}
 init(\var_1)\lor\cdots \lor init(\var_n)\lor\\
\align\hspace*{2em} \nonumber
 init(F)\land\neg [init(\phi_1)\lor\cdots \lor init(\phi_m)\lor
  succ(\phi_1')\lor\cdots \lor succ(\phi_k')],
\end{eqnarray}
which is the right side of the equivalence of the pseudo-successor
state axiom for $succ(F)$ in $Succ_A$.
\item Now suppose $M_2$ satisfies (\ref{eq1}). We'll show that $M_1$
  satisfies the right side of (\ref{eq2}), thus $M_1\models succ(\tau(F))$ so $M_2\models
  succ(F)$.
There are two cases:
\begin{itemize}
\item $M_2$ satisfies the following formula:
\begin{equation}\label{eq3}
 init(\var_1)\lor\cdots \lor init(\var_n).
\end{equation}
In this case, since the above formula does not mention any complex fluents
and has no quantifier, $M_1$ satisfies the following corresponding
formula:
\begin{equation}\label{eq4}
 init(\tau(\var_1))\lor\cdots \lor init(\tau(\var_n)).
\end{equation}
Thus $M_1$ satisfies the right side of  (\ref{eq2}).
\item $M_2$ does not satisfy (\ref{eq3}) but satisfies the following formula:
\[
 init(F)\land\neg [init(\phi_1)\lor\cdots \lor init(\phi_m)\lor
  succ(\phi_1')\lor\cdots \lor succ(\phi_k')].
\]
Thus $M_1$ satisfies the following formula:
\begin{eqnarray*}
\align
 init(\tau(F))\land\neg [init(\tau(\phi_1))\lor\cdots \lor init(\tau(\phi_m))\lor\\
\align\hspace*{5em}
  succ(\tau(\phi_1'))\lor\cdots \lor succ(\tau(\phi_k'))].
\end{eqnarray*}
So to show that the right side of the equivalence of (\ref{eq2}) is
satisfied by $M_1$, we need to show that $M_1\models \neg succ(\phi)$.
Recall that $\phi$ is a
disjunction such that each disjunct $\alpha$ must correspond to a
domain rule of the form $\causes(\alpha,\neg \tau(F))$, and that $\alpha$
is of the form $\alpha_1\land G$ such that $\alpha_1$ does not mention
fluents, and $G$ is a fluent atom that
mentions an
object that does not occur in $\tau(A)$.
Note that $init(\alpha)\supset \neg
init(\tau(F))$ is an axiom in $Succ_{\tau(A)}$, which is satisfied by
$M_1$. Thus $M_1\models \neg init(\alpha)$. This means that either
$\alpha_1$ or $init(G)$ is
false in $M_1$. If $\alpha_1$ is false, then $succ(\alpha)$ is false
since $succ(\alpha_1)$ is the same as $\alpha_1$.
Suppose that $init(G)$ is false in $M_1$. Notice that since there are
no positive domain rules, and that $G$ has an object not in $\tau(A)$
and $\tau(F)$, the pseudo-successor
state axiom for $G$ in $Succ_{\tau(A)}$ must be of the form $succ(G)\equiv
init(G)\land \Phi$.
Therefore from $M_1\models \neg init(G)$ we get
$M_1\models \neg succ(\alpha)$. 
Since $\alpha$ is any disjunct of $\phi$, we have
proved that $M_1\models \neg succ(\phi)$. Therefore $M_1\models
succ(\tau(F))$. Thus $M_2\models succ(F)$.
\end{itemize}
\end{itemize}
\end{proof}

\section{Related Work}


In planning, the most closely related work is the causal reasoning module
in Wilkins's SIPE system \cite{sipe}. Wilkins writes (page 85, \citeR{sipe}):
``Use of the STRIPS
assumptions has made operators unacceptably difficult to describe in
previous classical planners... One of the primary reasons for this is that
all effects of an action must be explicitly stated...
Deductive causal theories are one of the most important mechanisms used by
SIPE to alleviate problems in operator representation caused by the STRIPS
assumption.'' This is certainly one of the motivations for our
system as well. In SIPE, domain rules have triggers, preconditions,
conditions, and effects. Informally, when the triggers become true in
the new situation, SIPE would then check in sequence to see
 if the preconditions 
were true in the old situation, and the conditions are true in the
new situation. If all these conditions are true, it will then 
deduce the effects.
For instance, a SIPE causal rule for $on(x,y)$ in the blocks world
would look like:
\begin{verbatim}
Causal-rule: Not-on
Arguments: x, y, z;
Trigger: on(x,y);
Precondition: on(x,z);
Effects: not on(x,z);
\end{verbatim}
In comparison, our domain rules are much simpler. For instance, our
corresponding rule for the above SIPE rule is simply:
$\causes(on(x,y)\land y\neq z, on(x,z))$. We do not need procedural
directives like triggers. To a large degree, we can see our system as
a rational reconstruction of the causal reasoning module in SIPE.
As we have shown in Theorem \ref{soundness}, the procedure used by
our system is sound under a translation to causal 
theories in the situation calculus. While
Wilkins also gave a translation of his causal rules to formulas
in the situation calculus, he did not specify an underlying logic
to reason about such formulas. In fact, as shown by
\citeA{Lin:causality}, such translations would not work.

For those familiar with PDDL, the original version by
McDermott and the AIPS-98 Planning Competition Committee allows
domain axioms over stratified theories. According to the manual
of PDDL 1.2 \cite{McDermott:PDDL}, ``axioms are logical formulas
that assert relationships among propositions that hold within a situation.''
The format for writing axioms in PDDL is as follows:
\begin{verbatim}
(:axiom
  :vars (?x ?y ...)
  :context W
  :implies P)
\end{verbatim}
where $W$ is a formula and $P$ a literal. Axioms are treated directionally,
from $W$ to $P$. The following is the rule and intention for using the axioms
according to the manual:
\begin{quote}
``The rule is that action definitions are not allowed to have
effects that mention predicates that occur in the \verb-:implies- field of an
axiom. The intention is that action definitions mention `primitive' predicates
like $on$, and that all changes in truth value of `derived' predicates like 
$above$ occur through axioms. Without axioms, the action definitions will have to describe changes in all predicates that might be affected by an action, which leads to a complex software engineering (or 'domain engineering') problem.''
\end{quote}
It is clear from this quotation that axioms in PDDL are intended for 
defining ``derived'' predicates. They are similar to our complex fluent
definitions. New versions of PDDL have extended the original version by
allowing actions with durations and continuous changes. They have not 
considered using axioms to derive changes to ``primitive'' predicates like
what we have done here with domain rules.

Our action domain description language, while having a very different syntax
that is strongly influenced by Prolog syntax, shares much of the same
ideas behind action languages
\cite{GelfondLifschitz99}.
However, unlike action languages, ours
does not provide facilities
for expressing the truth value of a fluent atom in a particular
situation like the initial situation. Rather, it is aimed at specifying
the generic effects of actions. On the other hand, it has 
facilities for specifying types and static relations. 
Most importantly, to date,
action languages are either implemented directly or mapped to a nonmonotonic
logic programming system rather than by 
compilation into a monotonic system where action effects are given
explicitly, as is done here. For instance, a new SAT-based planning
method would have to be implemented \cite<e.g.>{McCainTurnerKR98} for
action languages. In comparison, once an action domain description is compiled
to a STRIPS-like description, existing planning systems such as Blackbox
\cite{SelmanKautz:blackbox} or System R \cite{Lin:R} can be directly called.

\section{Concluding Remarks}

We have described a system for generating the effects of actions from
direct action effect axioms and domain rules, among other things.
We have shown the soundness of the procedure used by the system
and tested it successfully in many benchmark action domains used by current AI
planners.
For future work, we are considering how to generalize the simple
action theories in Section~\ref{generalize} to include
context-dependent action domain descriptions like the monkey and
bananas domain.



\section*{Acknowledgments}

An extended abstract of part of this paper
  appeared in {\em Proceedings of AAAI-2000}.
I would like to thank 
the anonymous reviewers for
both JAIR and AAAI'2000 as well as the
associate editor in charge of this paper for JAIR
for their insightful comments on earlier versions
of this paper. This work was supported in part by
the Research Grants Council of Hong Kong
under Competitive Earmarked Research Grant
HKUST6061/00E.

\bibliography{ref}
\bibliographystyle{theapa}




\end{document}
