带延迟合一的Superposition（叠加）演算
Superposition with Delayed Unification
AI总结：
该研究将合一操作从原子步骤提升到演算层面，把合一算法步骤转化为推理步骤，证明了一阶叠加演算在这种延迟合一机制下仍保持完备性，讨论了其对标准一阶叠加的优势并给出实验评估，为依赖大量/无限合一符的演算提供了合一与推理交错的新思路。
摘要：
在经典的基于饱和的证明系统中，合一（unification）一直被视为原子操作。但我们也可以将合一移至演算层面，把合一算法的步骤转化为推理步骤。对于依赖返回规模庞大甚至无限的合一符集合的合一过程的演算而言，将合一整合到演算中，是一种让合一与推理交错推进的有吸引力的方法，例如AC-superposition（AC叠加）和higher-order superposition（高阶叠加）都适用这种思路。我们证明，将合一规则移至演算层面后，一阶superposition（叠加）演算仍保持完备性。我们讨论了该方法即便对标准一阶叠加演算也具备的若干优势，并提供了实验评估结果。
英文摘要：
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
