Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke:
Proving Termination of Integer Term Rewriting
In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasília, Brazil.
Lecture Notes in Computer Science 5595, pages 32-47, 2009. ©Springer-Verlag
When using rewrite techniques
for termination analysis of programs,
a main problem are pre-defined data types like integers.
We extend term rewriting by built-in integers and adapt the
dependency pair framework to prove termination of integer term
rewriting automatically.
[
BibTeX
|
Paper (ps.gz)
|
Paper (pdf)
|
Paper on SpringerLink
]