摘要完整性，形式化
摘要：完成是术语重写中最研究的技术之一，对于使用等式的自动推理至关重要。在本文中，我们提出了抽象完成的新的正确性证明，包括有限运行和无限运行。对于地面完成的特殊情况，我们提出了一种基于随机下降的新证明。此外，我们还将结果扩展到有序完成，这是完成的一个重要扩展，旨在产生初始方程的地面完整表示。我们提出了关于两种设置下有序完成的完备性的新证明。此外，我们还重新审视和扩展了M''etivier关于重写系统可规范性的结果。文章中所提出的所有证明都在Isabelle/HOL中进行了形式化。
作者：Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
论文ID：1802.08437
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22