Edinburgh Research Explorer

Turning Eureka Steps into Calculations in Automatic Program Synthesis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publicationProceedings of the UK IT 90 Conference
Publication statusPublished - 1990


A description is given of a technique called middle-out reasoning for the control of search in automatic theorem proving. The authors illustrate it 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 call eureka steps. Middle-out reasoning enables these eureka steps to be produced, automatically, as a side effect of non-eureka steps.

Download statistics

No data available

ID: 403047