Turning Eureka Steps into Calculations in Automatic Program Synthesis

Abstract

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.