The main ideas and axioms of the
formalization presented in this section
are taken from [7]. STRIPS
is a planning system that uses a database
of logical formulas
to represent information about a state.
Associated with each situation s is
a database of logical formulas
describing what holds at that situation.
The wff
is true if formula
f is in the database associated
with situation s.
Each action a has a precondition,
an add list and a delete list,
which are formally characterized by the
following atomic formulas:
(1) True(Prec(a,s)) is true provided
action a can be performed in situation
s ;
(2) Del(f,a,s) is true if formula f
is to be deleted when action a is
performed in situation s;
(3) Add(f,a,s) is true if formula f
is to be added when action a is performed
in situation s.
The function Result maps a situation s and an action a into the situation that results when action a is performed in situation s. The following axiom determines what formulas are in the database associated with the situation Result(a,s). If the precondition of action a is met at situation s, then the sentences on the delete list of a are deleted from the database, and the sentences on the add list of a are added to it.
