Abstract: | The task of constructing programs can be treated as a task of finding proofs in an appropriate logic. For recursive programs, the corresponding logic includes appropriate induction principles. We describe a system that automates program synthesis via theorem proving in this way, building on control strategies developed for verification proofs using proof plans. This involves some extensions to the planning system. The resultant system automates an approach to programming where program development and correctness proof proceed hand in hand, as advocated by Gries.
|