Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Logical Methods in Computer Science, 21(2), pp. 10:1-10:44, 2025.
pdf 
doi:10.46298/LMCS-21(2:10)2025
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"}