Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | 26th International Conference on Rewriting Techniques and Applications, RTA 2015 |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 160-176 |
| Number of pages | 17 |
| Volume | 36 |
| ISBN (Electronic) | 9783939897859 |
| DOIs | |
| Publication status | Published - 1 Jun 2015 |
| Event | 26th International Conference on Rewriting Techniques and Applications, RTA 2015 - Warsaw, Poland Duration: 29 Jun 2015 → 1 Jul 2015 |
Conference
| Conference | 26th International Conference on Rewriting Techniques and Applications, RTA 2015 |
|---|---|
| Country/Territory | Poland |
| City | Warsaw |
| Period | 29/06/15 → 1/07/15 |
Keywords
- Finite automata
- Non-termination
- Regular languages