基于签名的格罗布纳基算法的通用可执行形式化
A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms
摘要：
我们提出了一个通用的和可执行的形式化的基于签名的算法（如Faugère的$F_5$）计算格罗布纳基，以及他们的数学背景，在伊莎贝尔/HOL证明助手。就计算效率而言，所述算法是目前最公知的用于计算格罗布纳基的算法。正式的开发试图尽可能通用，推广大多数已知的基于签名的算法的变体，但同时实现的功能是有效地执行具体的输入，有效地计算机械验证的格罗布纳基。除了正确性外，形式化还证明了在一定条件下算法先验地检测和避免所有无用的归零，并返回最小的签名格罗布纳基.据我们所知，这里提出的形式化是唯一的形式化的签名为基础的格罗布纳基算法存在至今。
英文摘要：
We present a generic and executable formalization of signature-based algorithms (such as Faugère's $F_5$) for computing Gröbner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are currently the best known algorithms for computing Gröbner bases in terms of computational efficiency. The formal development attempts to be as generic as possible, generalizing most known variants of signature-based algorithms, but at the same time the implemented functions are effectively executable on concrete input for efficiently computing mechanically verified Gröbner bases. Besides correctness the formalization also proves that under certain conditions the algorithms a-priori detect and avoid all useless reductions to zero, and return minimal signature Gröbner bases. To the best of our knowledge, the formalization presented here is the only formalization of signature-based Gröbner basis algorithms in existence so far.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
