Satisfying KBO Constraints
Symbolic Computation
2007-05-23 v2 Logic in Computer Science
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.
Cite
@article{arxiv.cs/0608032,
title = {Satisfying KBO Constraints},
author = {Harald Zankl and Aart Middeldorp},
journal= {arXiv preprint arXiv:cs/0608032},
year = {2007}
}
Comments
15 pages