Automatic proof and automatic programming have always enjoyed a close relationship. We present a unification of proof planning (a knowledge-based approach to automated proof) and schema-guided synthesis (a knowledge-based approach to automatic programming). This unification enhances schema-guided synthesis with features of proof planning, such as the use of heuristics and the separation between object-level and meta-level reasoning. It enhances proof planning with features of schema-guided synthesis, such as reuse. It allows program schemas and heuristics to be implemented as proof planning methods. We aim particularly at implementation within the lambda-Clam proof planner, whose higher-order features are particularly appropriate for synthesis. Program synthesis and satisfaction of its proof obligations, such as verification conditions, matchings, or simplifications, are thus neatly integrated.
Available as compressed Postscript (66 kB, no cover)
Download BibTeX entry.