A deductive solution for plan generation (Q578927)

A new deductive solution of the well-known problem of generating plans for robots is presented. The solution uses the connection method and requires the description of the initial and final configuration to be expressed in terms of logical formulas of arbitrary structure. The set of admissible actions has to be formalized in terms of rules of the form \(A\to B\), where both A and B are also logical formulas of arbitrary structure. The formula A or B describes the configuration before or after execution of the respective action. When a description of the task is available in this form, any theorem prover may take this description as an input, provided that it enjoys the ability to mark instances of literals that got involved in the proof, and cannot use a marked literal again except upon backtracking. If the problem as stated has a solution, then a proof will be found that returns a term as its final result. This term identifies the sequence of actions to be carried out via the Skolem function associated with each of the rules. Finally, the 3-socks problem is described and solved by the same connection method as the robot plan generation problem.