Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL

Lukas Bulwahn, Alexander Krauss, Tobias Nipkow

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.

pdf (c) Springer Verlag


author={Lukas Bulwahn and Alexander Krauss and Tobias Nipkow},
title={Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs 2007)},
editor={K. Schneider and J. Brandt},