Details:
Title  Title: A New Proof for the Correctness of F5 (F5Like) Algorithms  Author(s)  Yao Sun, Dingkang Wang  Type  Manual  Abstract  The famous F5 algorithm for computing Gr\"obner basis was presented by Faug\`ere 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 F5like 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 (F5reduction) 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 nonincremental 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.  Keywords  Grobner basis, F5 algorithm, proof of correctness, variation algorithm  Length  27 
URL 
http://arxiv.org/abs/1004.0084 
Language  English  Year  2010  Month  June  Translation 
No  Refereed 
No 
