Proving non-termination by finite automata

J. Endrullis, H. Zantema

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)
66 Downloads (Pure)


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 languageEnglish
Title of host publicationRewriting Techniques and Applications (26th International Conference, RTA'15, Warsaw, Poland, June 29-July 3, 2015)
EditorsM. Fernández
Place of PublicationDagstuhl
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Print)978-3-939897-85-9
Publication statusPublished - 2015
Event26th International Conference on Rewriting Techniques and Application (RTA 2015) - Warsaw, Poland
Duration: 2 Jun 20151 Jul 2015

Publication series

NameLIPIcs: Leibniz International Proceedings in Informatics
ISSN (Print)1868-8968


Conference26th International Conference on Rewriting Techniques and Application (RTA 2015)
Abbreviated titleRTA 2015


Dive into the research topics of 'Proving non-termination by finite automata'. Together they form a unique fingerprint.

Cite this