MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Kraan, Ina
Basin, David A.
Bundy, Alan		dblp
dblp
dblp
Editor(s):
Lau, K. K.
Clement, T.		dblp
dblp
BibTeX cite key*:
KraanBasinBundy93a
Title, Booktitle
Title*:
Logic Program Synthesis via Proof Planning
Booktitle*:
International Workshop on Logic Program Synthesis and Transformation (LOPSTR '92)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Manchester, UK
Language:
English
Event Date*
(no longer used):
1992
Organization:
Event Start Date:
14 May 2024
Event End Date:
14 May 2024
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Volume:
Number:
Month:
June
Pages:
1-14
Year*:
1993
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
Note:
Also available as Research Report MPI-I-92-244
(LaTeX) Abstract:
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 \overrightarrow{args.} prog(\overrightarrow {args}) \leftrightarrow spec(\overrightarrow{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.
Download
Access Level:

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:



BibTeX Entry:
@INPROCEEDINGS{KraanBasinBundy93a,
AUTHOR = {Kraan, Ina and Basin, David A. and Bundy, Alan},
 EDITOR = {Lau, K. K. and Clement, T.},
 TITLE = {Logic Program Synthesis via Proof Planning},
 BOOKTITLE = {International Workshop on Logic Program Synthesis and Transformation (LOPSTR '92)},
 PUBLISHER = {Springer},
 YEAR = {1993},
 PAGES = {1--14},
 ADDRESS = {Manchester, UK},
 MONTH = {June},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm		Created
01/14/1995 06:52:11 PM
Revisions
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Edit Dates
28.08.2001 08:40:26
21/01/95 20:53:03
17/01/95 19:28:16
14/01/95 19:00:53