Abstract

This article presents three 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 or linear arithmetic and the resulting formula is tested for satisfiability using dedicated solvers. 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. This means that in contrast to the dedicated methods our approach does not directly solve the problem but transforms it to equivalent formulations for which sophisticated back-ends exist. In order to make all approaches complete we present a method to compute upper bounds on the weights. Furthermore, our encodings take dependency pairs into account to increase the applicability of the order.

BibTeX Entry

@article{ZHM-JAR09,
 author    = "Harald Zankl and Nao Hirokawa and Aart Middeldorp",
 title     = "KBO Orientability",
 journal   = "Journal of Automated Reasoning",
 volume    = 43,
 number    = 2,
 pages     = "173-201",
 year      = 2009,
 doi       = "10.1007/s10817-009-9131-z"
}