cl-banner

Maximal Termination

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

Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 110 – 125, 2008.

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.

 

  PDF |    doi:10.1007/978-3-540-70590-1_8  |  ©  Springer

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"
}
Nach oben scrollen