@inproceedings{702713407da04dd58f316acf9397d434,
title = "Middle-Out Reasoning for Logic Program Synthesis",
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 verication proof. The approach is a two-level one: At the object level, we prove program verication conjectures in a sorted, rst-order theory. The conjectures are of the form 8args ! : prog(args ! ) $ spec(args ! ). At the meta-level, we plan the object-level verication with an unspecied program denition. The denition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning.",
keywords = "logic program synthesis, proof planning, Automated theorem proving",
author = "I. Kraan and D. Basin and Alan Bundy",
year = "1993",
language = "English",
isbn = "9780262731058",
booktitle = "Proceedings of the Tenth International Conference on Logic Programming",
publisher = "MIT Press",
}