Sciweavers

CADE
2007
Springer

Proving Termination by Bounded Increase

14 years 5 months ago
Proving Termination by Bounded Increase
Abstract. Most methods for termination analysis of term rewrite systems (TRSs) essentially try to find arguments of functions that decrease in recursive calls. However, they fail if the reason for termination is that an argument is increased in recursive calls repeatedly until it reaches a bound. In this paper, we solve that problem and show how to prove innermost termination of TRSs with bounded increase automatically.
Jürgen Giesl, René Thiemann, Stephan S
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CADE
Authors Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp
Comments (0)