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

Research Paper #448

Title:Turning Eureka Steps into Calculations in Automatic Program Synthesis
Authors:Bundy,A; Smaill,AD; Hesketh,J
Date: 1989
Presented:Submitted to UK-IT-90
Abstract:We describe a technique called middle-out reasoning for the control of search in automatic theorem proving. We illustrate its use in the domain of automatic program synthesis. Programs can be synthesised from proofs that their logical specifications are satisfiable. Each proof step is also a program construction step. Unfortunately, a naive use of this technique requires a human or computer to produce proof steps which provide the essential structure of the desired program. It is hard to see the justification for these steps at the time that they are made; the reason for them emerges only later in the proof. Such proof steps are often called 'eureka' steps. Middle-out reasoning enables these eureka steps to be produced, automatically, as a side effect of non-eureka steps.

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