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补全进行模拟。特别地，该结果允许我们在补全过程中的任意时刻从前一系统切换至后一系统。