Abstract

In this paper we consider a hierarchy of three versions of Knuth-Bendix
orders. (1) We show that the standard definition can be (slightly)
simplified without affecting the ordering relation. (2) For the extension
of transfinite Knuth-Bendix orders we show that transfinite ordinals
are not needed as weights, as far as termination of finite rewrite systems
is concerned. (3) Nevertheless termination proving benefits from
transfinite ordinals when used in the setting of general Knuth-Bendix
orders defined over a weakly monotone algebra. We investigate the
relationship to polynomial interpretations and present experimental
results for both termination analysis and ordered completion. For the
latter it is essential that the order is totalizable on ground terms.

BibTeX

@inproceedings{SWHZAM-LPAR18,
  author    = "Sarah Winkler and Harald Zankl and Aart Middeldorp",
  title     = "Ordinals and {Knuth-Bendix} Orders",
  booktitle = "Proceedings of the 18th International Conference on Logic
               for Programming, Artificial Intelligence, and Reasoning",
  series    = "Lecture Notes in Computer Science (Advanced Research in
               Computing and Software Science)",
  volume    = 7180,
  pages     = "420--434",
  year      = 2012
}