Overview of Strips Control
An operator is needed only if
a subgoal cannot be proven from the current model of the situation.
(Proof is carried out using a resolution theorem prover where
the current model, Mi, is used as the basis for the axioms
used in the proof. Note that the well-formed-formula (wffs) that
one tries to prove are either the goal wff or precondition
wffs.
The operators are scanned to
identify an operator whose add list specifies clauses that would
allow the proof to be successfully continued (if not completed).
When an add list is found whose clauses permit an adequate continuation
of the proof, then the associated operator is declared relevant...the
substitutions used in the proof continuation serve to at least
partially instantiate the arguments of the operator. The inner
loop of STRIPS is described as:
(1) Select a subgoal and try
to establish that it is true in the appropriate model. If it
is, then go to Step 4.
Otherwise:
(2) Choose as a relevant operator
one whose add list specifies clauses that allow the incomplete
proof of Step 1 to be continued.
(3) The appropriately instantiated
precondition wff of the selected operator constitutes a new subgoal.
Go to Step 1.
(4) If the subgoal is the main
goal, terminate, Otherwise, create a new model by applying the
operator whose precondition is the subgoal just established.
Go to Step 1.
[ The search can be
Represented as an AND/OR tree where step 2, at least implicitly,
gives the OR, the list of relevant operators, and step 2 chooses
one of these...Step 3 does the AND expansion...Step 1 tests for
satisfaction and if True goes to step 4 the model is mapped from
Mi -> Mi+1. Mi+1 would be "passed" back up to the
parent node and control goes again to Step 1 to retest for satisfaction
of the parent subgoal in this new model. ]
The output of STRIPS is a list
of instantiated operators whose corresponding actions will achieve
the goal.
|
