Finding lexicographic orders for termination proofs in Isabelle/HOL
Lukas Bulwahn, Alexander Krauss, Tobias Nipkow
Abstract
We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice.
Publication
In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science, pages 38–53. Springer Verlag