Abstract

We consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We further present new complexity results. An extension reflecting the recent proposal of subterm coefficients in standard Knuth-Bendix orders is also given. The various orders are compared on problems in termination and completion.

BibTeX

@inproceedings{AYSWNHAM-FLOPS14,
  author    = "Akihisa Yamada and Sarah Winkler and Nao Hirokawa and
               Aart Middeldorp",
  title     = "{AC-KBO} Revisited",
  booktitle = "Proceedings of the 12th International Symposium on
               Functional and Logic Programming",
  editor    = "Michael Codish and Eijiro Sumii",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  volume    = 8475,
  pages     = "319--335"
  year      = 2014,
  doi       = "10.1007/978-3-319-07151-0"
}