MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


Logic program synthesis via proof planning

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

October 1992, 14 pages.

Status: available - back from printing

We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At the object level, we prove program verification conjectures in a sorted, first-order theory. The conjectures are of the form $\forall \vec{args}. \; prog(\vec{args}) \leftrightarrow spec(\vec{args})$. At the meta-level, we plan the object-level verification with an unspecified program definition. The definition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning. This technique is an application of the Clam proof planning system. Clam is currently powerful enough to plan verification proofs for given programs. We show that, if Clam's use of middle-out reasoning is extended, it will also be able to synthesize programs.

  • MPI-I-92-244.pdfMPI-I-92-244.pdfMPI-I-92-244.dvi
  • Attachement: MPI-I-92-244.dvi (54 KBytes); MPI-I-92-244.pdf (101 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Kraan, Ina and Basin, David A. and Bundy, Alan},
  TITLE = {Logic program synthesis via proof planning},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-244},
  MONTH = {October},
  YEAR = {1992},
  ISSN = {0946-011X},