cl-banner

Satisfying KBO Constraints

Harald Zankl and Aart Middeldorp

Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 389 – 403, 2007.

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.

 

  PDF |    doi:10.1007/978-3-540-73449-9_29  |  © Springer

BibTeX 

@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",
publisher = "Springer-Verlag",
year = 2007,
volume = 4533,
pages = "389--403"
}
Nach oben scrollen