Termination of Integer Term Rewriting

Authors Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, Stephan Falke

Thumbnail PDF


  • Filesize: 87 kB
  • 4 pages

Document Identifiers

Author Details

Carsten Fuhs
Jürgen Giesl
Martin Plücker
Peter Schneider-Kamp
Stephan Falke

Cite AsGet BibTex

Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke. Termination of Integer Term Rewriting. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Recently, techniques and tools from term rewriting have been successfully applied to prove termination automatically for different programming languages. The advantage of rewrite techniques is that they are very powerful for algorithms on user-defined data structures. But in contrast to techniques for termination analysis of imperative programs, the drawback of rewrite techniques is that they do not support data structures like integer numbers which are pre-defined in almost all programming languages. To solve this problem, we extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically. Our experiments show that this indeed combines the power of rewrite techniques on user-defined data types with a powerful treatment of pre-defined integers.
  • Termination analysis
  • integers
  • term rewriting
  • dependency pairs


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail