Abstract

Most techniques to automatically disprove termination of term rewrite systems search for a loop. Whereas a loop implies non-termination for full rewriting, this is not necessarily the case if one considers rewriting under strategies. Therefore, in this paper we first generalize the notion of a loop to a loop under a given strategy. In a second step we present two novel decision procedures to check whether a given loop is a context-sensitive or an outermost loop. We implemented and successfully evaluated our method in the termination prover TTT2.

BibTeX

@inproceedings{RTCS-RTA09,
author      = "Ren{\'e} Thiemann and Christian Sternagel",
title       = "Loops under Strategies",
booktitle   = "Proceedings of the 20th International Conference on Rewriting
               Techniques and Applications",
series      = "Lecture Notes in Computer Science",
publisher   = "Springer-Verlag",
volume      = 5595,
pages       = "17--31",
year        = 2009
}