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

@inproceedings{HZCSAM-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
}