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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp
• Keywords: Automated Reasoning, CADE 2007, Recursive Calls, Term Rewrite Systems, Termination Analysis