Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL

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.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Lukas Bulwahn, Alexander Krauss, Tobias Nipkow
• Keywords: Artificial Intelligence, Lexicographic Combinations, Simple Method, Theorem Proving Practice, TPHOL 2007