Abstract

This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in (pseudo-)propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such that the induced Knuth-Bendix order orients the rules of the encoded rewrite system from left to right.

BibTeX Entry

@inproceedings{ZM-RTA07,
 author    = "Harald Zankl and Aart Middeldorp",
 title     = "Satisfying {KBO} Constraints",
 booktitle = "Proceedings of the 18th International Conference on Rewriting
              Techniques and Applications",
 series    = "Lecture Notes in Computer Science",
 volume    = 4533,
 pages     = "389--403",
 year      = 2007,
 doi       = "10.1007/978-3-540-73449-9\_29"
}