The following axioms allow us to define
precisely the space of mental situations.
We use variables for
blocks (*x*, *y*, *z*, *w*, ...), for
situations (*s*, , ...), for
actions (*a*, , ...), for mental
situations (*m*, , ...), for
mental actions ( , ,
...), for formulas in the database (*f*,
, ...), for subgoals -formulas
in the goal stack- (*g*,
, ...), for sequences of actions,
(*r*, , ...), and for sequences of
mental actions (*l*, , ...).

We assume uniqueness of names for
every function symbol *h*, and every pair
of distinct function symbols *h* and *g*.
The symbols *h* and *g* are syntactical
variables ranging over distinct function
symbols; the symbols to are
syntactical variables ranging over block
constants. Axiom
defines the expression
[12], which means that
mental situation can be
*reached* from mental situation
*m* by executing a nonempty sequence
of *appropriate* mental actions
( is an abbreviation for
). We include
domain closure axioms for blocks,
mental situations, actions, and mental
actions. Axiom of
induction allows us to prove that a
property holds for all mental
situations that are reachable from
a given mental situation.

Tue Jul 21 09:26:01 PDT 1998