@INPROCEEDINGS{KraanBasinBundy93b,
AUTHOR        = {Ina Kraan and David Basin and Alan Bundy},
TITLE         = {Middle-Out Reasoning for Logic Program Synthesis},
BOOKTITLE     = {Proc.~10th Intern. Conference on Logic Programing (ICLP '93)} #
 " {\rm (Budapest, Hungary)}",
ADDRESS       = {Cambridge, MA},
PUBLISHER     = {{MIT} {P}ress},
YEAR          = {1993},
PAGES         = {441--455},
NOTE          = {Also available as Technical Report MPI-I-93-214},
ABSTRACT      = {
Logic programs can be synthesized as a by-product of the
planning of their verification proofs. This is achieved
by using higher-order variables at the proof planning level,
which become instantiated in the course of planning. We
illustrate two uses of such variables in proof planning
for program synthesis, one for synthesis proper and one
for the selection of induction schemes. We demonstrate that
the use of these variables can be restricted naturally in
such a way that terms containing them form a tractable extension
of first-order terms.},
}