@MISC{POLYRED.MIZ,
  AUTHOR = {Schwarzweller, Christoph},
  TITLE = {Polynomial Reduction},
  SECTION1 = {Preliminaries},
  SECTION2 = {More on Polynomials and Monomials},
  SECTION3 = {Multiplication of Polynomials with Bags},
  SECTION4 = {Orders on Polynomials},
  SECTION5 = {Polynomial Reduction},
  SECTION6 = {Polynomial Reduction Relation},
  DAY = {20},
  MONTH = {December},
  YEAR = {2002},
  ADDRESS1 = {University of Tuebingen},
  SUMMARY = {We continue the formalization of \cite{Becker93} towards Gr\"obner Bases. In
this article we introduce reduction of polynomials and prove its termination,
its adequateness for ideal congruence as well as the translation lemma used 
later to show confluence of reduction.}}

