Abstract

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.

BibTeX Entry

@inproceedings{ZSM-WFLP08,
 author    = "Harald Zankl and Christian Sternagel and Aart Middeldorp",
 title     = "Transforming {SAT} into Termination of Rewriting",
 booktitle = "Proceedings of the 17th International Workshop on Functional
              and (Constraint) Logic Programming",
 series    = "Electronic Notes in Theoretical Computer Science",
 volume    = 246,
 pages     = "199--214",
 year      = 2009,
 doi       = "10.1016/j.entcs.2009.07.023"
}