基于签名的Gr"obner基算法的通用可执行形式化
摘要：在Isabelle/HOL证明助手中，我们提出了一种通用且可执行的签名算法（如Faug`ere's $F\_5$）的形式化，用于计算Gr"obner基以及其数学背景。这些算法目前是计算Gr"obner基的计算效率最好的已知算法。该形式化开发尝试尽可能通用，概括了大多数已知的基于签名的算法的变种，但同时实现的函数在具体输入上是有效可执行的，用于高效计算机验证的Gr"obner基。除了正确性外，该形式化还证明了在某些条件下，算法先验地检测和避免了所有无用的归零缩减，并返回最小签名Gr"obner基。据我们所知，这里所呈现的形式化是迄今存在的唯一的基于签名的Gr"obner基算法的形式化。
作者：Alexander Maletzky
论文ID：2012.02239
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2020-12-15