Top-down Synthesis of Recursive Logic Procedures from 
First-order Logic Specifications

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, England.
kung-kiu@cs.man.ac.uk

Steve Prestwich
European Computer-Industry Research Center
Arabellastrasse 17, D-8000 Munchen 81, West Germany

Abstract:
Derivation of logic programs from first-order logic specifications is 
nontrivial and tends to be done by hand. We describe a method for 
synthesising recursive logic procedures from their first-order logic 
specifications that is amenable to mechanisation.  The method is
strictly top-down  and has been implemented as part of a user-guided 
synthesis system in Prolog.