Details:
Title  A new proof for the correctness of the F5 algorithm.  Author(s)  Yao Sun, Dongming Wang  Type  Article in Journal  Abstract  In 2002, Faugère presented the famous F5 algorithm for computing Gröbner basis where two criteria, syzygy criterion and rewritten criterion, were proposed to avoid redundant computations. He proved the correctness of the syzygy criterion, but the proof for the correctness of the rewritten criterion was left. Since then, F5 has been studied extensively. Some proofs for the correctness of F5 were proposed, but these proofs are valid only under some extra assumptions. In this paper, we give a proof for the correctness of F5B, an equivalent version of F5 in Buchberger’s style. The proof is valid for both homogeneous and nonhomogeneous polynomial systems. Since this proof does not depend on the computing order of the Spairs, any strategy of selecting Spairs could be used in F5B or F5. Furthermore, we propose a natural and nonincremental variant of F5 where two revised criteria can be used to remove almost all redundant Spairs.  Keywords  Gröbner basis, F5, F5B, correctness of F5  ISSN  16747283; 18691862/e 
URL 
http://link.springer.com/article/10.1007%2Fs1142501244801 
Language  English  Journal  Sci. China, Math.  Volume  56  Number  4  Pages  745756  Publisher  Springer, Berlin/Heidelberg; Science in China Press, Beijing  Year  2013  Edition  0  Translation 
No  Refereed 
No 
