Transforming SAT into Termination of Rewriting

Harald Zankl, Christian Sternagel, and Aart Middeldorp

Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), Electronic Notes in Theoretical Computer Science 246, pp. 199 – 214, 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.


  PDF |    doi:10.1016/j.entcs.2009.07.023  |  © 2009 Elsevier B.V.


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
Nach oben scrollen