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

BibTeX: 

@inproceedings{KraussBN-TPHOLs07,
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},
publisher=Springer,series=LNCS,volume={4732},pages={38-53},year=2007}