23 Feb
2007
23 Feb
'07
16:00
The following technical report is available from http://aib.informatik.rwth-aachen.de:
Proving Termination by Bounded Increase Jürgen Giesl, René Thiemann, Stephan Swiderski, and Peter Schneider-Kamp AIB 2007-03
Most methods and tools 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 present a method to prove termination of TRSs with bounded increase automatically.