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 |
| Keywords: | |
| 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}