AIB 2008-03: Maximal Termination

The following technical report is available from http://aib.informatik.rwth-aachen.de:

Maximal Termination Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl AIB 2008-03

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.