抽象完备化，形式化
Abstract Completion, Formalized
AI总结：
本文提出了抽象完备化（含有限与无限运行）及有序完备化的新正确性证明，并扩展了规范性结果，所有证明已在Isabelle/HOL中形式化。
摘要：
完备化是项重写中研究最深入的技术之一，也是基于等式的自动推理的基础。在本文中，我们提出了抽象完备化的新正确性证明，涵盖有限运行和无限运行两种情况。对于地面完备化的特例，我们提出了一种基于随机下降的新证明。此外，我们将结果扩展到有序完备化，这是完备化的一种重要扩展，旨在生成初始等式的完备化表示。我们针对两种设置提出了关于有序完备化完备性的新证明。此外，我们重新审视并扩展了Métivier关于重写系统规范性的结果。本文中所有证明均已在Isabelle/HOL中形式化。
英文摘要：
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
