Construction of Gröbner Bases: Avoiding S-Polynomials– Buchberger’s First Criterium

Abstract

We continue the formalization of Groebner bases following the book “Groebner Bases– A Computational Approach to Commutative Algebra” by Becker and Weispfenning. Here we prove Buchberger’s first criterium on avoiding S-polynomials: S-polynomials for polynomials with disjoint head terms need not be considered when constructing Groebner bases. In the course of formalizing this theorem we also introduced the splitting of a polynomial in an upper and a lower polynomial containing the greater resp. smaller terms of the original polynomial with respect to a given term order.