AC-KBO Revisited

Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp

Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Lecture Notes in Computer Science 8475, pp. 319 – 335, 2014.


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.


  PDF |    doi:10.1007/978-3-319-07151-0  |  © Springer International Publishing Switzerland 2014


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"
Nach oben scrollen