Construction of Grobner Bases: Avoiding S-Polynomials - Buchberger's First Criterium 1
Christoph Schwarzweller · 2005
Summary. 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.