The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

PhD Thesis #9425

Title:Proof Planning for Logic Program Sythesis
Authors:Kraan,I
Date: 1994
Presented:
Keywords:
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. Middle-out reasoning uses variables to represent unknown details of a proof. Unification 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 CLAM [Bundy et al 90c], called periwinkle, which has been used to synthesize a variety of programs fully automatically.
Download:NO ONLINE COPY

[Search These Pages] [DAI Home Page] [Comment]