Program schemas as proof methods.
Julian Richardson, Pierre Flener · 2003
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.