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 in which a given goal formula can be proven to be true. STRIPS represents a world model as an arbitrary collection in first-order predicate calculus formulas and is designed to work with models consisting of large numbers of formula. It employs a resolution theorem prover to answer questions of particular models and uses means-ends analysis to guide it to the desired goal-satisfying model.

Cite

Text

Fikes and Nilsson. "STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving." International Joint Conference on Artificial Intelligence, 1971. doi:10.1016/0004-3702(71)90010-5

Markdown

[Fikes and Nilsson. "STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving." International Joint Conference on Artificial Intelligence, 1971.](https://mlanthology.org/ijcai/1971/fikes1971ijcai-strips/) doi:10.1016/0004-3702(71)90010-5

BibTeX

@inproceedings{fikes1971ijcai-strips,
  title     = {{STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving}},
  author    = {Fikes, Richard and Nilsson, Nils J.},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1971},
  pages     = {608-620},
  doi       = {10.1016/0004-3702(71)90010-5},
  url       = {https://mlanthology.org/ijcai/1971/fikes1971ijcai-strips/}
}