Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:


URL for downloading the paper:


Event Address*:

Manchester, UK

Language:

English

Event Date*
(no longer used):

1992

Organization:


Event Start Date:

15 November 2019

Event End Date:

15 November 2019

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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