Abstract

We revisit completion modulo equational theories for
left-linear term rewrite systems where unification modulo the theory
is avoided and the normal rewrite relation can be used in order to
decide validity questions. To that end, we give a new correctness
proof for finite runs and establish a simulation result between the
two inference systems known from the literature. Given a concrete
reduction order, novel canonicity results show that the resulting
complete systems are unique up to the representation of their rules’
right-hand sides. Furthermore, we show how left-linear AC
completion can be simulated by general AC completion. In particular,
this result allows us to switch from the former to the latter at any
point during a completion process.

BibTeX

@article{NHM-LMCS21,
 author    = "Johannes Niederhauser and Nao Hirokawa and Aart Middeldorp",
 title     = "Left-Linear Completion with {AC} Axioms",
 journal   = "Logical Methods in Computer Science",
 volume    = 21,
 number    = 2,
 pages     = "10:1--10:44",
 year      = 2025,
 doi       = "10.46298/LMCS-21(2:10)2025"
}