MPI-INF/SWS Research Reports 1991-2021

2. Number - only D2


Middle-out reasoning for logic program synthesis

Basin, David A. and Kraan, Ina and Bundy, Alan

April 1993, 12 pages.

Status: available - back from printing

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.

  • MPI-I-93-214.pdfMPI-I-93-214.pdfMPI-I-93-214.dvi
  • Attachement: ATTL9WOS (55 KBytes); MPI-I-93-214.pdf (104 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Basin, David A. and Kraan, Ina and Bundy, Alan},
  TITLE = {Middle-out reasoning for logic program synthesis},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-214},
  MONTH = {April},
  YEAR = {1993},
  ISSN = {0946-011X},