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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Giesl, J., Thiemann, R., Swiderski, S., & Schneider-Kamp, P. (2007). Proving termination by bounded increase. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 443–459). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_33
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
