An ordinal measure based procedure for termination of functions

AbstractThis paper describes a method for proving termination of recursively defined functions based on ordinal measure. It generalizes a termination procedure developed by Manoury and Simonot initially for an automated program synthesis system called ProPre. For that, we associate ordinal functions to formal proofs made in the system and show that they follow a decreasing property. In this way, after having translated the recursive functions in the Boyer–Moore theorem prover, it is shown that each ordinal coming from the ProPre system can be given to the theorem prover as a well-founded ordering which allows it to prove in its turn the termination