A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.
|Name||LIPIcs: Leibniz International Proceedings in Informatics|
|Conference||26th International Conference on Rewriting Techniques and Application (RTA 2015)|
|Abbreviated title||RTA 2015|
|Period||2/06/15 → 1/07/15|