Automatizing termination proofs of recursively defined functions

AbstractThis paper describes a fully automated strategy for proving termination of functions defined by recursive equations. This strategy has been implemented in the ProPre program synthesis system as one of the mechanism that leads from specifications of functions to programs. It has been successfully tested on the Ackerman function, a functional specification of the quick-sort and various other standard functional algorithms