Transforming SAT into Termination of Rewriting
Harald Zankl, Christian Sternagel, Aart Middeldorp · Electronic Notes in Theoretical Computer Science · 2009
In this paper we propose different translations from SAT to termination of term rewriting, i.e., we translate a propositional formula φ into a generic rewrite system R φ with the property that φ is satisfiable if and only if R φ is (non)terminating. Our experiments reveal that the generated rewrite systems are challenging for automated termination provers. Furthermore, a large class of them seems to be just unprovable by current methods implemented in termination analyzers.