约化环上的Buchberger算法
Verifying Buchberger's Algorithm in Reduction Rings
摘要：
在本文中，我们提出了正式的，计算机支持的验证功能实现的布赫伯格的临界对/完成算法计算格罗布纳基在减少环。我们描述了如何在一个单一的软件系统，这在我们的情况下是定理系统的算法可以实现和验证。与已有的Buchberger算法在其他系统中的形式正确性证明相比，e. G. Coq和ACL 2，我们的工作不限于经典的设置多项式环的领域，但考虑更一般的设置约简环，这，自然，使算法更复杂，验证更困难。正确性证明主要是基于约化环理论中的一些非平凡结果，我们对这些结果进行了形式化和形式化证明。这种形式化已经包含了800多个交互式证明的引理和定理，使阐述成为Theorma中高阶理论探索的广泛例子。
英文摘要：
In this paper we present the formal, computer-supported verification of a functional implementation of Buchberger's critical-pair/completion algorithm for computing Gröbner bases in reduction rings. We describe how the algorithm can be implemented and verified within one single software system, which in our case is the Theorema system. In contrast to existing formal correctness proofs of Buchberger's algorithm in other systems, e. g. Coq and ACL2, our work is not confined to the classical setting of polynomial rings over fields, but considers the much more general setting of reduction rings; this, naturally, makes the algorithm more complicated and the verification more difficult. The correctness proof is essentially based on some non-trivial results from the theory of reduction rings, which we formalized and formally proved as well. This formalization already consists of more than 800 interactively proved lemmas and theorems, making the elaboration an extensive example of higher-order theory exploration in Theorema.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
