F5（F5-Like）算法正确性的新证明
A New Proof for the Correctness of F5 (F5-Like) Algorithm
摘要：
著名的计算格罗布纳基的F5算法是由Faugère于2002年提出的，但没有完整地证明其正确性。本文作者将原F5算法简化为Buchberger式的F5算法（F5 B算法），它与原F5算法等价，并可能推出一些类似F5的算法。本文简要回顾了F5 B算法，并对F5 B算法的正确性提出了一个新的完整证明。这种新的证明不限于齐次系统，也不依赖于选择临界对的策略（即决定首先计算哪个临界对的策略），使得任何策略都可以在F5 B（F5）算法中使用。从这个新的证明中，我们发现特殊的约简过程（F5-约简）是F5算法的关键，因此保持这种特殊的约简，各种变异算法就变得可用。提出了F5算法的一种自然变形，将原F5算法转化为一种非增量算法，并给出了证明。这种自然的变化已经在布尔环上实现。在这种自然变化中的两个修正准则也能够拒绝几乎所有不必要的计算，并且在大多数例子中很少有多项式减少到0。
英文摘要：
The famous F5 algorithm for computing Gröbner basis was presented by Faugère in 2002 without complete proofs for its correctness. The current authors have simplified the original F5 algorithm into an F5 algorithm in Buchberger's style (F5B algorithm), which is equivalent to original F5 algorithm and may deduce some F5-like versions. In this paper, the F5B algorithm is briefly revisited and a new complete proof for the correctness of F5B algorithm is proposed. This new proof is not limited to homogeneous systems and does not depend on the strategy of selecting critical pairs (i.e. the strategy deciding which critical pair is computed first) such that any strategy could be utilized in F5B (F5) algorithm. From this new proof, we find that the special reduction procedure (F5-reduction) is the key of F5 algorithm, so maintaining this special reduction, various variation algorithms become available. A natural variation of F5 algorithm, which transforms original F5 algorithm to a non-incremental algorithm, is presented and proved in this paper as well. This natural variation has been implemented over the Boolean ring. The two revised criteria in this natural variation are also able to reject almost all unnecessary computations and few polynomials reduce to 0 in most examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
