- ...formulas
- The
formalization presented applies only to
a simplified version of STRIPS in which
we allow only atomic formulas in the
database, add and delete lists of the
actions, and in the stack describing the
goal configuration. These conditions can
be relaxed as shown in [4].
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...wff
- The function
*DB*maps a reified formula of the sort database*f*and a situation*s*into a reified formula of the sort goal stack.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
*s* - The function
*Prec*maps an action*a*and a situation*s*into a reified formula of the sort goal stack.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...8#8
- The variables
*i*and 8#8 range over natural numbers and situations, respectively.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...subgoal
- The intuition
behind the formalization of subgoals as
reified formulas of the form 13#13
is that the problem would be solved if
the formulas in the stack describing
the problem's goal situation were true
in the problem's initial situation.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...subgoals
- These are the
subgoals that would have been below
*a*if the top subgoal of the goal stack had been replaced by action*a*(step 1 of the algorithm).. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...subgoals
- The expressions
*At*(*g*,*s*) and 29#29 are defined as follows: (1) 30#30; and (2) 31#31.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...situation
- In this case, the
location numbers of the subgoals
in
*GS*are the same as the location numbers of the formulas they refer to in the stack describing 6#6.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...stack
- A subgoal
is above another subgoal in the goal stack
if its location number is smaller than the
location number of the second subgoal.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...length
- We use the following
abbreviations 57#57, and
58#58. The length
of a mental situation is defined as follows:
(1) 59#59;
(2) 60#60.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
*N* - The
constant
*N*is a natural number describing the threshold of the depth first search strategy used by STRIPS, i.e., the maximum depth to which it explores the tree of mental situations.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

- ...
*Quote*(*Prec*(*a*,*s*)) - These
expressions represent the subgoals that
proposition
*p*is in the database associated with situation*s*, or that the precondition of action*a*holds at situation*s*.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Tue Jul 21 09:26:01 PDT 1998