An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details. The method is illustrated by the automatic construction of both recursive and iterative programs operating on natural numbers, lists, and trees.
Reasoning about actions necessarily involves tracking the truth of assertions about the world over time. The SIPE planning system retains the efficiency of the STRIPS assumption for this while enhancing expressive power by allowing the specification of a causal theory.
