论文标题
基于签名的Gröbner基础算法的通用和可执行的形式化
A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms
论文作者
论文摘要
我们提出了一种基于签名的算法（例如Faugère的$ f_5 $）的通用和可执行式的形式化，用于计算Gröbner基础以及其数学背景，以及Isabelle/Hol Proof Assistant中的数学背景。在计算效率方面，说算法是计算Gröbner基础的最著名算法。正式的开发试图尽可能通用，从而概括了基于签名的算法的大多数已知变体，但与此同时，实现的函数在混凝土输入上有效地可执行，以有效地计算机械验证的Gröbner碱基。除了正确性外，形式化还证明，在某些条件下，A算法A-Priori检测并避免所有无用的减少降低到零，并返回最小的签名Gröbner基础。 据我们所知，这里提出的形式化是迄今为止存在的基于签名的Gröbner基础算法的唯一形式化。
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.
