Abstract

We present the first method to disprove innermost termination of term rewrite systems automatically. To this end, we first develop a suitable notion of an innermost loop. Second, we show how to detect innermost loops: One can start with any technique amenable to find loops. Then our novel procedure can be applied to decide whether a given loop is an innermost loop. We implemented and successfully evaluated our method in the termination prover AProVE.

BibTeX

@inproceedings{RTJGPS-RTA08,
author      = "Ren{\'e} Thiemann and J{\"u}rgen Giesl and Peter
               Schneider-Kamp",
title       = "Deciding Innermost Loops",
booktitle   = "Proceedings of the 19th International Conference on Rewriting
               Techniques and Applications",
series      = "Lecture Notes in Computer Science",
volume      = 5117,
publisher   = "Springer-Verlag",
year        = 2008,
pages       = "366--380"
}