一句话：为左线性项重写系统在 AC 公理下的完成过程给出新的正确性证明、模拟关系与典范性结果。
本文重新审视左线性项重写系统在等式理论（尤其是 AC 公理）下的完成问题。与通常需要模理论合一的方法不同，该工作避免模理论合一，转而利用普通重写关系判定有效性。作者为有限运行给出新的正确性证明，并在文献中两个推理系统之间建立模拟结果；给定具体约简序后，新的典范性结果说明所得完成系统在规则右端表示意义下唯一。进一步，作者证明左线性 AC 完成可由一般 AC 完成模拟，从而可在完成过程中任意时刻从前者切换到后者。评估以形式证明、模拟与唯一性定理为主。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NiederhauserHM25,
title = {Left-Linear Completion with AC Axioms},
author = {Johannes Niederhauser and Nao Hirokawa and Aart Middeldorp},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:10)2025}
}