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

@article{HZNHAM-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
}