AC-KBO Revisited

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

Theory and Practice of Logic Programming 16(2), pp. 163 – 188, 2016.


Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this paper 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 version, 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.1017/S1471068415000083  |  © Cambridge University Press 2015


author = "Akihisa Yamada and Sarah Winkler and Nao Hirokawa and Aart Middeldorp",
title = "{AC-KBO} Revisited",
journal = "Theory and Practice of Logic Programming",
volume = 16,
issue = 2,
pages = "163--188"
year = 2016,
doi = "10.1017/S1471068415000083"
Nach oben scrollen