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 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.

BibTeX

@inproceedings{CFJGAMPSRTHZ-RTA08,
author      = "Carsten Fuhs and J{\"u}rgen Giesl and Aart Middeldorp and
               Peter Schneider-Kamp and Ren{\'e} Thiemann and Harald Zankl",
title       = "Maximal Termination",
booktitle   = "Proceedings of the 19th International Conference on Rewriting
               Techniques and Applications",
series      = "Lecture Notes in Computer Science",
volume      = 5117,
publisher   = "Springer-Verlag",
year        = 2008,
pages       = "110--125"
}