Synthesis of a Family of Recursive Sorting Procedures

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

Abstract:
In an earlier paper, we described a method for synthesising recursive 
logic procedures from their first-order logic specifications.  The
method is practical because it is strictly top-down   and has been
implemented as part of a user-guided synthesis system in Prolog. We
have used the system to  synthesise procedures for a wide variety of 
algorithms, including a large family of recursive sorting
procedures. In this paper we describe the synthesis of this family of 
procedures.