264 Chapter 12 Control Strategies in Deductive Planning
1. Plans as programs. In this approach, the user does not specify a goal and ask
the theorem prover to find a plan by deduction. One rather writes programs in
a logical language that are possibly incomplete specifications of plans. This can
reduce significantly the search for a proof because the theorem prover needs
to find a proof only for those parts of the plan that are not fully specified.
For instance, rather than giving to the planner the goal “the robot should be
loaded at a target location,” the user can write a program “move the robot
to an intermediate location, find a plan for loading the robot and move the
robot to the target location.”
2. Tactics. Tactics are user-defined programs that specify ...