Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Logic program synthesis via proof planning

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

MPI-I-92-244. October 1992, 14 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-244.pdfMPI-I-92-244.pdfMPI-I-92-244.dvi54 KBytes; 101 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
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},