2015/05/03 by Jörg Endrullis, Endrullis, Jörg, Hans Zantema +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1505.00478
arxiv created 2015/05/03 · openalex publication_date 2015/05/03 · arxiv updated 2015/05/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.