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

Inside the paper

The problem

A robot planning a sequence of actions must reason about the state of its world and how that state changes. General theorem proving can express such problems, but a practical search also needs a way to choose actions and manage their effects.

The idea

STRIPS combines a theorem prover with a search through world models. It uses differences between the current model and a goal to select relevant operators and builds subgoals for their preconditions.

How it works

• The world model describes facts about the current situation, while a goal is expressed as a condition to be proved from that model.
• A difference between the model and goal helps select an operator whose effects could reduce that difference.
• The planner tries to establish the chosen operator’s preconditions, making subsidiary plans when those conditions do not already hold.
• Applying an operator updates the model by deleting and adding specified facts, so subsequent search considers the resulting situation.

What it showed

The paper describes an implementation and examples including robot tasks involving rooms, boxes and a light switch. These examples demonstrate the planner’s operation on its stated representations, while the authors also discuss limitations and future work.

Read it for

Start with Sections 2.1 and 2.2 for the world model and search strategy, then follow the worked example in Section 3.5. Section 4 gives larger tasks; the implementation details in Sections 3.1–3.4 can be skimmed until the example raises a specific question.

Written in our own words from the paper itself. A draft the editors have not yet reviewed.