The F5 criterion revised

This paper introduces some new concepts that place the criterion in a more general setting: S-Gröbner bases and primitive S-irreducible polynomials. We use these to propose a new, simple algorithm based on a revised F5 criterion. The new concepts also enable us to remove various restrictions, such as proving termination without the requirement that f1,…,fm be a regular sequence.