@MISC{GROEB_3.MIZ,
  AUTHOR = {Schwarzweller, Christoph},
  TITLE = {Construction of {G}r\"obner Bases:
       Avoiding S-Polynomials -- {B}uchberger's First Criterium},
  NOTE = {This work has been partially supported by grant BW 5100-5-0147-4.},
  SECTION1 = {Preliminaries},
  SECTION2 = {More on Polynomials},
  SECTION3 = {Restriction and Splitting of Polynomials},
  SECTION4 = {More on Polynomial Reduction},
  SECTION5 = {The Criterium},
  DAY = {10},
  MONTH = {December},
  YEAR = {2004},
  ADDRESS1 = {University of Gda\'{n}sk},
  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.}}

