Logic Program Synthesis via Proof Planning

I. Kraan, D. Basin, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 ∀−→−−args.prog(−→−−args)↔spec(−→−−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 [Bundy et al 90c]. 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.
Original languageEnglish
Title of host publicationLogic Program Synthesis and Transformation
Subtitle of host publicationProceedings of LOPSTR 92, International Workshop on Logic Program Synthesis and Transformation, University of Manchester, 2-3 July 1992
PublisherSpringer London
Pages 1-14
ISBN (Electronic)978-1-4471-3560-9
ISBN (Print)978-3-540-19806-2
Publication statusPublished - 1993

Publication series

NameWorkshops in Computing
PublisherSpringer London
ISSN (Print)1431-1682


Dive into the research topics of 'Logic Program Synthesis via Proof Planning'. Together they form a unique fingerprint.

Cite this