TY - GEN
T1 - Middle-Out Reasoning for Logic Program Synthesis
AU - Kraan, I.
AU - Basin, D.
AU - Bundy, Alan
PY - 1993
Y1 - 1993
N2 - 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.
AB - 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.
KW - logic program synthesis
KW - proof planning
KW - Automated theorem proving
M3 - Conference contribution
SN - 9780262731058
BT - Proceedings of the Tenth International Conference on Logic Programming
PB - MIT Press
ER -