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.

翻译：本文重新审视了左线性项重写系统在等式理论下的补全方法，该方法避免了模理论统一，并利用正规重写关系判定有效性。为此，我们给出了有限运行的新正确性证明，并对文献中已知的两种推理系统建立了模拟关系。基于具体归约序，新的规范性结果表明：所得完备系统在规则右端表示意义下具有唯一性。此外，我们证明了左线性AC补全可通过一般AC补全进行模拟。特别地，该结果允许我们在补全过程中的任意时刻从前一种方法切换至后一种方法。