✍ Scribed by François Monin; Marianne Simonot
No coin nor oath required. For personal study only.
This paper describes a method for proving termination of recursively deÿned 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.
📜 SIMILAR VOLUMES
Some applications of the GUHA method of mechanized hypothesis formation in pedagogy, economics and sports are described with emphasis on constructions of two-valued data models. The adequacy of the used procedures is partly discussed on the basis of concrete results and in the comparison with other