# AC-KBO Revisited

arXiv: https://arxiv.org/abs/1403.0406 · HTML: https://mlsanity.com/paper/1403.0406/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Mar 2014.

## Built on by (most cited first, 1 of 1)

- [Automated Strategy Invention for Confluence of Term Rewrite Systems](https://mlsanity.com/paper/2411.06409/) (2024)

## Abstract (arXiv)

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.