max planck institut
informatik

MPI-I-92-244

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.
Acknowledgement:
References to related material:

MPI-I-92-244.pdf54 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: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-244
BibTeX
@TECHREPORT{KraanBasinBundy92,
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},