Show simple item record

Proceedings of the UK IT 90 Conference

dc.contributor.authorBundy, Alan
dc.contributor.authorSmaill, A.
dc.contributor.authorHesketh, J.
dc.date.accessioned2010-12-21T14:30:30Z
dc.date.available2010-12-21T14:30:30Z
dc.date.issued1990
dc.identifier.urihttp://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=114292&tag=1en
dc.identifier.urihttp://hdl.handle.net/1842/4557
dc.description.abstractA 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.en
dc.language.isoenen
dc.titleTurning Eureka Steps into Calculations in Automatic Program Synthesisen
dc.typeConference Paperen
rps.titleProceedings of the UK IT 90 Conferenceen
dc.extent.noOfPages221-226en
dc.extent.pageNumbers221–226en
dc.date.updated2010-12-21T14:30:31Z
dc.date.openingDate1990-03-19
dc.date.closingDate1990-03-22


Files in this item

This item appears in the following Collection(s)

Show simple item record