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 Entry

@article{NHM-LMCS25,
 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"
}