A new proof for the correctness of the F5 algorithm (Q365812)

This paper is devoted to the proof of the correctness of the F5 algorithm for computing Gröbner bases proposed in [\textit{J.-C. Faugère}, Proceedings of the 2002 international symposium on symbolic and algebraic computation, Lille, France, July 07--10, 2002. New York, NY: ACM Press. 75--83 (2002; Zbl 1072.68664)]. (The work by J.-C. Faugère does not contain a rigorous proof of the correctness of the algorithm.) The paper under review presents an algorithm F5B, which is an equivalent version of F5, and gives a complete proof the correctness of F5B. The structure of the paper is as follows. The first part (section 2) introduces the concepts of \(S\)-pairs and \(S\)-polynomials of labeled polynomials, as well as the notions of F5-divisibility, F5-rewritability, and F5-reduction of labeled polynomials. Using these concepts, the authors simplify algorithm F5 ``in Buchberger style'' and obtain its equivalent version F5B. Then the authors prove some results on labeled polynomials (section 3) and use them to provide a complete proof of algorithm F5B (section 4). The last part of the work introduces variants of the F5 algorithm where the results of the paper (mainly, the results on the F5-reduction) allow one to reject almost all redundant \(S\)-pairs in the Gröbner basis computation process.