Maximal Termination

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp,
René Thiemann, Harald Zankl

We present a new approach for termination proofs that uses polynomial
interpretations (with possibly negative coefficients) together with the
"maximum" function. To obtain a powerful automatic method, we solve two
main challenges: (1) We show how to adapt the latest developments in the
dependency pair framework to our setting. (2) We show how to automate
the search for such interpretations by integrating "max" into recent
SAT-based methods for polynomial interpretations.  Experimental results
support our approach.