STRIPS: a new approach to the application of theorem proving to problem solving
Richard Fikes, Nils J. Nilsson
Abstract
Richard Fikes, Nils J. Nilsson
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
OpenAlex reports 1480 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
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
Key concepts: STRIPS, First-order logic, Problem solver, Automated theorem proving, Solver, Calculus (dental), Resolution (logic), Computer science