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

Research Paper #729

Title:Middle-Out Reasoning for Synthesis and Induction
Authors:Kraan,I; Basin,D; Bundy,A
Date:Aug 1995
Presented:Published in the Journal of Automated Reasoning, Special Issue "Automated Mathematical Induction" vol. 16, Nos. 1-2, March '96, pgs. 113-145, ed. H. Zhang
Keywords:automated theorem proving, proof planning, induction, logic program synthesis, meta-variables
Abstract:We develop two applications of middle-out reasoning in inductive proofs: Logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al [Bundy et al 90a]. Middle-out reasoning uses variables to represent unknown terms and formulae. 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 during synthesis is difficult, because the recursion of 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 that are applied to 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. We have implemented these techniques as an extension of the proof planning system CLAM [Bundy et al 90c], called Periwinkle, and synthesized a variety of programs fully automatically.
Download:POSTSCRIPT COPY

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