Satisfying KBO Constraints
符号计算
2007-05-23 v2 计算机科学中的逻辑
摘要
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.
引用
@article{arxiv.cs/0608032,
title = {Satisfying KBO Constraints},
author = {Harald Zankl and Aart Middeldorp},
journal= {arXiv preprint arXiv:cs/0608032},
year = {2007}
}
备注
15 pages