@inproceedings{3256514f0c594fdbb24a8612072fb0ed,
title = "Logic Program Synthesis via Proof Planning",
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 ∀−→−−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.",
author = "I. Kraan and D. Basin and Alan Bundy",
year = "1993",
doi = "10.1007/978-1-4471-3560-9_1",
language = "English",
isbn = "978-3-540-19806-2",
series = "Workshops in Computing",
publisher = "Springer London",
pages = "1--14",
booktitle = "Logic Program Synthesis and Transformation",
address = "United Kingdom",
}