AC-KBO revisited*†. Issue 2 (8th June 2015)

• Record Type: Journal Article
• Authors: YAMADA, AKIHISA; WINKLER, SARAH; HIROKAWA, NAO; MIDDELDORP, AART
• Is Part Of: Theory and practice of logic programming. Volume 16:Issue 2(2016)
• Page Start: 163
• Page End: 188
• Publication Date: 2015-06-08
• Subjects: Term rewriting, -- termination, -- associative-commutative theory, -- Knuth-Bendix order; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068415000083
• Languages: English
• ISSNs: 1471-0684

Abstract

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.