de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Middle-out reasoning for logic program synthesis

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44204

Bundy,  Alan
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

MPI-I-93-214.pdf
(Any fulltext), 105KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Basin, D. A., Kraan, I., & Bundy, A.(1993). Middle-out reasoning for logic program synthesis (MPI-I-93-214). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B445-C
Abstract
Logic programs can be synthesized as a by-product of the planning of their verification proofs. This is achieved by using higher-order variables at the proof planning level, which become instantiated in the course of planning. We illustrate two uses of such variables in proof planning for program synthesis, one for synthesis proper and one for the selection of induction schemes. We demonstrate that the use of these variables can be restricted naturally in such a way that terms containing them form a tractable extension of first-order terms.