一句话：在 Isabelle/HOL 中形式化抽象完成、有序完成与 Métivier 正则性结果，并给出新的正确性证明。
本文研究项重写与等式自动推理中的完成（completion）技术。作者为抽象完成在有限和无限运行下的正确性给出新证明；针对 ground completion，提出基于随机下降（random descent）的新证明；并将结果扩展到 ordered completion，证明其在两种设置下关于生成初始等式的 ground-complete 表示具有完备性；同时重新审视并扩展 Métivier 关于重写系统 canonicity 的结果。所有证明均已在 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\'etivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
@article{paperbot766,
title = {Abstract Completion, Formalized},
author = {Nao Hirokawa and Aart Middeldorp and Christian Sternagel and Sarah Winkler},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:19)2019}
}