On The Criteria Of The F5 Algorithm

TL;DR

This paper provides proofs for both the F5 and Rewritten Criteria in Faugere's F5 algorithm, clarifying their connection to syzygies and illustrating their application with examples, aiming to enhance understanding and potential improvements.

Contribution

It offers the first proof of the Rewritten Criterion, linking both criteria to syzygies, and discusses potential improvements and implementation details.

Findings

Proof of the Rewritten Criterion established

Connection between criteria and syzygies clarified

Implementation insights provided for F5 in SINGULAR

Abstract

Faugere's F5 algorithm is one of the fastest known algorithms for the computation of Grobner bases. So far only the F5 Criterion is proved, whereas the second powerful criterion, the Rewritten Criterion, is not understood very well until now. We give a proof of both, the F5 Criterion and the Rewritten Criterion showing their connection to syzygies, i.e. the relations between the S-Polynomials to be investigated by the algorithm. Using the example of a Grobner basis computation stated in Faugere's F5 paper we show how the criteria work, and discuss the possibility of improving the F5 Criterion. An introduction to a SINGULAR implementation of F5 is given in the end.