STRIPS: a new approach to the application of theorem proving to problem solving

Abstract

We describe a new problem solver called STRIPS that attempts to find a sequence of operators in a space of world models to transform a given initial world model into a model in which a given goal formula can be proven to be true. STRIPS represents a world model as an arbi trary collection of first-order predicate calculus formulas and is designed to work with models consisting of 1arge numbers of formulas. 1t employs a resolution theorem p rover to answer (jues t ions of particular models and uses means-ends analysis to guide it to the desired goal-satisfying model. DESCRIPTIVE TERMS Probl em solv J ng, t heorem prov i rig, robot