Elamur Research⌕
☰
home / papers / 1971 / STRIPS: A new approach to the application of theorem proving to problem solving

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

Paper · 1971 · Richard E. Fikes and Nils J. Nilsson

Summary

Fikes and Nilsson present STRIPS (STanford Research Institute Problem Solver), a planner for robot tasks such as moving objects and navigating between rooms. These tasks need far richer state descriptions than puzzles or games. Earlier work by Green relied purely on theorem proving to find operator sequences, but it stalled on the frame problem. STRIPS instead keeps two activities apart. A resolution theorem prover only answers questions inside a single world model: which operators apply, and whether the goal already holds. A GPS-style means-ends analysis searches across models. World models are sets of first-order predicate calculus formulas (wffs). Operators are grouped into parameterized schemata, each with a precondition wff schema and lists of formulas to add and delete. When a proof attempt fails, the unfinished proof serves as the "difference" to reduce. Relevant operators are then selected, and their preconditions become subgoals. On three robot tasks the search stayed tightly focused on the goal. This made STRIPS a foundational template for later AI planning representations.

Key points

  • STRIPS was implemented in LISP on a PDP-10 and used in SRI robot research. Theorem proving was done with QA3.5, which consumed most of the run time.
  • Problem space has three parts: an initial world model (a set of wffs), operators (preconditions plus add/delete effects), and a goal wff.
  • Search builds a tree of nodes, each pairing a world model with an ordered goal list. An evaluation function considers subgoal count and difficulty, operator cost, and difference complexity.
  • Test tasks used operators such as gotol, goto2, and pushto. Total CPU times were roughly 113.1 s for turning on a lightswitch, 66.0 s for pushing three boxes together, and 123.0 s for reaching a location in another room. Theorem proving accounted for about 83.0, 49.6, and 104.9 s respectively.
  • The search is largely depth-first, so solutions can be non-optimal (as in the lightswitch task). Planned extensions include conditionals and loops, program synthesis, and learning generalized new operators.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🔬SRI InternationalMenlo Park · United States24 works · 12,175 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputer Networks and Communications · 100 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Richard E. Fikes and Nils J. Nilsson. 1971. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{fikes1971strips,
  title = {{STRIPS: A new approach to the application of theorem proving to problem solving}},
  author = {Richard E. Fikes and Nils J. Nilsson},
  booktitle = {Artificial Intelligence},
  year = {1971},
  doi = {10.1016/0004-3702(71)90010-5},
  url = {https://doi.org/10.1016/0004-3702(71)90010-5}
}

References

11 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Nilsson, N. J. Problem.Solving Methods in Artificial Intelligence. McGraw-Hill Book Company, New Y~rk, New York, 1971. find
  2. Munson, J. H. Robot planning, execution, and monitoring in an uncertain environment. Proc. 2nd Int'l. Joint Conf. Artificial Intelligence, London, England (September 13, 1971). find
  3. Fikes, R. E. Monitored execution of robot plans produced by STRIPS. Proc. IFIP 71, Ljubljana, Yugoslavia (August 1971). find
  4. Green, C. Application of theorem proving to problem solving. Proc. Int'l. Joint Conf. Artificial Intelligence, Washington, D.C. (May 1969). find
  5. Raphael, B. The frame problem in problem-solving systems. Proc. Adv. Study In_vt. on Artificial Intelligence and Heuristic Programming, Menaggio, Italy (August 1970). find
  6. Ernst, G. and .~4ewell, A. GPS: A Case Study in Generality and Problem Solving. ACM Monograph Series. Academic Press, New York, New York, 1969. find
  7. Garvey, T. and Kling, R. User's guide to QA3.5 Question-Answering System. Stanford Research Institute Artificial Intelligence Group Technical Note 15, Menlo Park, California [December 1969). find
  8. Waldinger, R. and Lee, R. PROW: A step toward automatic program writing. Proc. lnt'l. Conf. Artificial Intelligence, Washington, D.C. (May 1969). find
  9. Manna, Z. and Waldinger, R. Towards automatic program synthes,.%. Comm. ACM. 14, No. 3 (March 1971). find
  10. Hart, P. E. and Nilsson~ N. J. The constt, tion of generalized plans as an approach toward learning. Stanford Research Instit..'. Artificial Intelligence Group Memo, Menlo Park, California (5 April 1971). find
  11. Hewitt, C. PLANNER: A language for Manipulating models and proving theorems in a robot. Artificial Intelligence Memo No. 168 (Revised), Project MAC, Massachusetts Institute of Technology, Cambridge, Massachusetts (August 1970). Artificial Intelligence 2 (1971), 189-208 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/fikes-1971-strips-new-approach-application-theorem/