Maximal termination

Abstract. 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 de-velopments 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.