MPI-I-92-244
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.pdf
- Attachement: MPI-I-92-244.dvi (54 KBytes); MPI-I-92-244.pdf (101 KBytes)
URL to this document: https://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},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-92-244},
MONTH = {October},
YEAR = {1992},
ISSN = {0946-011X},
}