We present a declarative
formalization of STRIPS in the
*situation calculus*.
This section outlines its main
components and features, at the
same time that describes the
structure of the paper.

First, we present a
*situation calculus* formalization
of the STRIPS representation of planning
problems. This formalization is proposed
in [7], and it is
characterized by making the STRIPS database
explicit and reifying the formulas that are
in the database. This allows handling
deletions, and quantifying over those
formulas. Then, we describe the situations,
actions, and strategy STRIPS uses to reason
about those representations of planning
problems. Instead of formalizing a reasoning
strategy as a meta-theory of the object-theory
describing a planning problem [3],
we introduce the concepts of *mental
situations* and *mental actions* as first
order objects of the language. This allows us
to formalize in a single theory the dynamics
of both: (1) the object situations STRIPS
reasons about, which describe a particular
planning problem; and (2) the mental
situations it constructs to reason about
that problem.

The formalization of the reasoning strategy
used by STRIPS (*goal stack planning*)
is presented in two stages. First, we define
the *space of mental situations* on
which that reasoning strategy operates. The
formalization of mental situations makes the
goal stack explicit, and represents subgoals
as reified formulas describing the formulas
that should and should not be in the
database associated with a given situation.
The reasoning process performed by STRIPS
is explained in terms of a single type of
mental action, *Hyp(a)*, which denotes
the mental act of hypothesizing the
execution of action *a* at a particular
point of the plan currently being
constructed. Later on in the paper,
we introduce *backtracking*
actions which allow retracting wrong
hypotheses about actions. Then, we
describe the *heuristics* and
*search strategy* STRIPS uses
to explore the space
of mental situations. In particular,
we provide axiomatizations of:
(1) depth first search (with backtracking);
and (2) some of the *heuristics* used by
STRIPS for selecting actions and
detecting *dead-ends* during the
searching process. [15] shows how
this simple formalization accounts for the
standard STRIPS solution to the blocks world
problem known as Sussman's anomaly. The
successive mental situations constructed by
STRIPS in the process of searching for that
solution, and the interaction between such
mental situations and the object situations
(hypothetical solutions) they reason about
are described in detail.

The ideas about the formalization of
individual concepts and propositions
in [6] are used to
distinguish between the fact described
by a formula and its truth value. In
particular, we use a reified formula to
represent the fact described by a
formula, and the predicate *True*
to assert the fact described
by that formula. Thus *True*(*p*) is true
iff the fact described by the reified
formula *p* is true. We use two subsorts
of variables for reified formulas: *f*
for formulas in the *database*; and
*g* for formulas in the *goal stack*.

Tue Jul 21 09:26:01 PDT 1998