Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
Journal of Automated Reasoning Volume 53, Number 3, pp. 219 – 244, 2016.
pdf 
doi:10.1007/s10817-016-9362-8
Abstract
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.
BibTex
@article{DBLP:journals/jar/BlanchetteGKKU16, author = {Jasmin Christian Blanchette and David Greenaway and Cezary Kaliszyk and Daniel K{\"{u}}hlwein and Josef Urban}, title = {A Learning-Based Fact Selector for Isabelle/HOL}, journal = {J. Autom. Reasoning}, volume = {57}, number = {3}, pages = {219--244}, year = {2016}, url = {http://dx.doi.org/10.1007/s10817-016-9362-8}, doi = {10.1007/s10817-016-9362-8}, timestamp = {Mon, 05 Sep 2016 19:00:15 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/jar/BlanchetteGKKU16}, bibsource = {dblp computer science bibliography, http://dblp.org}}