...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.
```.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
```

Josefina Sierra
Tue Jul 21 09:26:01 PDT 1998