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 Entry

@inproceedings{YWHM-FLOPS14,
 author    = "Akihisa Yamada and Sarah Winkler and Nao Hirokawa and Aart
              Middeldorp",
 title     = "{AC--KBO} Revisited",
 booktitle = "Proceedings of the 12th International Conference on
              Functional and Logic Programming",
 series    = "Lecture Notes in Computer Science",
 volume    = 8475,
 pages     = "319--335",
 year      = 2014,
 doi       = "10.1007/978-3-642-28717-6\_33"
}