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.
