Abstract
The area of logic program synthesis is attracting increased interest. Most efforts
have concentrated on applying techniques from functional program synthesis to
logic program synthesis. This thesis investigates a new approach: Synthesizing
logic programs automatically via middle-out reasoning in proof planning.
[Bundy et al 90a] suggested middle-out reasoning in proof planning. Middleout
reasoning uses variables to represent unknown details of a proof. Unifica¬
tion instantiates the variables in the subsequent planning, while proof planning
provides the necessary search control.
Middle-out reasoning is used for synthesis by planning the verification of an
unknown logic program: The program body is represented with a meta-variable.
The planning results both in an instantiation of the program body and a plan for
the verification of that program. If the plan executes successfully, the synthesized
program is partially correct and complete.
Middle-out reasoning is also used to select induction schemes. Finding an
appropriate induction scheme in synthesis is difficult, because the recursion in
the program, which is unknown at the outset, determines the induction in the
proof. In middle-out induction, we set up a schematic step case by representing
the constructors applied to the induction variables with meta-variables. Once
the step case is complete, the instantiated variables correspond to an induction
appropriate to the recursion of the program.
The results reported in this thesis are encouraging. The approach has been
implemented as an extension to the proof planner CUM [Bundy et al 90c], called
Periwinkle, which has been used to synthesize a variety of programs fully automatically.
