@PhdThesis{Buchberger1965,
  Title                    = {{Ein Algorithmus zum Auffinden der Basiselemente 
des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm 
for Finding the Basis Elements in the Residue Class Ring Modulo a Zero 
Dimensional Polynomial Ideal)}},
  Author                   = {Bruno Buchberger},
  School                   = {Mathematical Institute, University of Innsbruck, 
Austria},
  Year                     = {1965},
  Note                     = {English translation in \emph{Journal of Symbolic 
Computation} 41(3--4):475--511, Special Issue on Logic, Mathematics, and 
Computer Science: Interactions}
}

@Article{Buchberger1970,
  Title                    = {{Ein algorithmisches Kriterium f\"ur die 
L\"osbarkeit eines algebraischen Gleichungssystems (An Algorithmic Criterion for 
the Solvability of an Algebraic System of Equations)}},
  Author                   = {Bruno Buchberger},
  Journal                  = {Aequationes Mathematicae},
  Year                     = {1970},
  Note                     = {(English translation in \emph{Gr\"obner Bases and 
Applications (Proceedings of the International Conference ``33 Years of 
Gr\"obner Bases'', 1998)}, London Mathematical Society Lecture Note Series 251, 
Cambridge Univerity Press, 1998, pages 535--545)},
  Pages                    = {374--383},
  Publisher                = {Birkh\"auser}
}

@InProceedings{Buchberger1979,
  Title                    = {{A Criterion for Detecting Unnecessary Reductions 
in the Construction of Gr\"obner Bases}},
  Author                   = {Bruno Buchberger},
  Booktitle                = {{Symbolic and Algebraic Computation 
(Proceedings of EUROSAM'79, Marseille, June 26-28)}},
  Year                     = {1979},
  Editor                   = {Edward W. Ng},
  Pages                    = {3--21},
  Publisher                = {Springer},
  Series                   = {Lecture Notes in Computer Science},
  Volume                   = {72},
  Doi                      = {10.1007/3-540-09519-5_52}
}

@inproceedings{Winkler1983,
  title = {{A Criterion for Eliminating Unnecessary Reductions in the 
Knuth-Bendix Algorithm}},
  author = {Franz Winkler and Bruno Buchberger},
    booktitle = {{Proceedings of Algebra and Logic in Computer Science, 
Gy\H{o}r, Hungary}},
  series = {Colloquia Mathematica Societatis Janos Bolyai},
  volume = {42},
  pages = {849--869},
  publisher = {North Holland},
  year = {1983},
  editor = {J. Demetrovics and G. Katona and A. Salomaa},
  url = {http://www.risc.jku.at/publications/download/risc_231/1983-09-00-A.pdf}
}

@Article{Robbiano1985,
  Title                    = {{On the Theory of Graded Structures}},
  Author                   = {Lorenzo Robbiano},
  Journal                  = {Journal of Symbolic Computation},
  Year                     = {1985},
  Pages                    = {138--170},
  Volume                   = {2},
  Publisher                = {Elsevier},
  Doi                      = {10.1016/S0747-7171(86)80019-0}
}

@Book{Adams1994,
  Title                    = {{An Introduction to Gr\"obner Bases}},
  Author                   = {William W. Adams and Philippe Loustaunau},
  Publisher                = {American Mathematical Society},
  Year                     = {1994},
  Month                    = {July}
}

@ARTICLE{Mora1994,
  author = {Teo Mora},
  title = {{An Introduction to Commutative and Non-Commutative Gr\"obner 
Bases}},
  journal = {Theoretical Computer Science},
  year = {1994},
  volume = {134},
  pages = {131--173},
  number = {1},
  publisher = {Elsevier},
  doi = {10.1016/0304-3975(94)90283-6}
}

@InCollection{Buchberger1998a,
  Title                    = {{Introduction to Gr\"obner Bases}},
  Author                   = {Bruno Buchberger},
  Editor                   = {Bruno Buchberger and Franz Winkler},
  Publisher                = {Cambridge University Press},
  Year                     = {1998},
  Series                   = {London Mathematical Society Lectures Notes 
Series},
  Number = {251},
  Booktitle                = {Gr\"obner Bases and Applications},
  Pages                    = {3 - 31}
}

@article{Faugere1999,
  title = {{A New Efficient Algorithm for Computing Gr\"obner Bases ($F_4$)}},
  author = {Jean-Charles Faug\`ere},
  journal = {Journal of Pure and Applied Algebra},
  publisher = {Elsevier},
  volume = {139},
  number = {1},
  pages = {61--88},
  year = {1999},
  doi = {10.1016/S0022-4049(99)00005-5}
}

@Book{Kreuzer2000,
  Title                    = {{Computational Commutative Algebra 1}},
  Author                   = {Martin Kreuzer and Lorenzo Robbiano},
  Publisher                = {Springer-Verlag},
  Year                     = {2000}
}

@article{Thery2001,
  author = {Laurent Th\'ery},
  title = {{A Machine-Checked Implementation of Buchberger's Algorithm}},
  journal = {Journal of Automated Reasoning},
  year = {2001},
  volume = {26},
  number = {2},
  pages = {107--137},
  publisher = {Springer},
  doi = {10.1023/A:1026518331905}
}

@inproceedings{Faugere2002,
  title = {{A New Efficient Algorithm for Computing Gr\"obner Bases without Reduction to Zero 
($F_5$)}},
  author = {Jean-Charles Faug\`ere},
  editor = {Teo Mora},
  booktitle = {{Proceedings of ISSAC'02}},
  publisher = {ACM Press},
  pages = {61--88},
  year = {2002}
}

@TechReport{Buchberger2003,
  Title                    = {{Gr\"obner Rings in Theorema: A Case Study in Functors and Categories}},
  Author                   = {Bruno Buchberger},
  Institution              = {Johannes Kepler University Linz, Spezialforschungsbereich F013},
  Year                     = {2003},
  Month                    = {November},
  Number                   = {2003-49},
  HowPublished             = {SFB Report}
}

@inproceedings{Schwarzweller2006,
  author = {Christoph Schwarzweller},
  title = {{Gr\"obner Bases -- Theory Refinement in the Mizar System}},
  booktitle = {Mathematical Knowledge Management (4th International Conference, 
Bremen, Germany, July 15--17)},
  year = {2006},
  editor = {Michael Kohlhase},
  volume = {3863},
  series = {Lecture Notes in Artificial Intelligence},
  pages = {299--314},
  publisher = {Springer},
  doi = {10.1007/11618027_20}
}

@INPROCEEDINGS{Chaieb2007,
  author = {Amine Chaieb and Makarius Wenzel},
  title = {{Context aware Calculation and Deduction: Ring Equalities via 
{Gr\"obner Bases} in Isabelle}},
  booktitle = {{Towards Mechanized Mathematical Assistants (Proceedings of 
Calculemus'2007, Hagenberg, Austria, June 27--30)}},
  year = {2007},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang 
Windsteiger},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {4573},
  pages = {27--39}
}

@article{Jorge2009,
  author = {J. Santiago Jorge and Victor M. Guilas and Jose L. Freire},
  title = {{Certifying properties of an efficient functional program for 
computing Gr\"obner bases}},
  journal = {Journal of Symbolic Computation},
  year = {2009},
  volume = {44},
  pages = {571--582},
  number = {5},
  publisher = {Elsevier},
  doi = {10.1016/j.jsc.2007.07.016}
}

@article{Medina-Bulo2010,
  author = {Inmaculada Medina-Bulo and Francisco Palomo-Lozano and Jose-Luis 
Ruiz-Reina},
  title = {{A verified \textsc{Common Lisp} implementation of Buchberger's 
algorithm in ACL2}},
  journal = {Journal of Symbolic Computation},
  year = {2010},
  volume = {45},
  pages = {96--123},
  number = {1},
  publisher = {Elsevier},
  doi = {10.1016/j.jsc.2009.07.002}
}

@article{Sternagel2010,
  author  = {Christian Sternagel and Ren\'e Thiemann},
  title   = {{Executable Multivariate Polynomials}},
  journal = {Archive of Formal Proofs},
  year    = {2010},
  note    = {\url{http://isa-afp.org/entries/Polynomials.shtml},
            Formal proof development},
  ISSN    = {2150-914x}
}

@article{Sternagel2012,
  author  = {Christian Sternagel},
  title   = {{Well-Quasi-Orders}},
  journal = {Archive of Formal Proofs},
  year    = {2012},
  note    = {\url{http://isa-afp.org/entries/Well_Quasi_Orders.shtml},
            Formal proof development},
  ISSN    = {2150-914x}
}

@phdthesis{Maletzky2016b,
  title = {{Computer-Assisted Exploration of Gr\"obner 
Bases Theory in Theorema}},
  author = {Alexander Maletzky},
  school = {Research Institute for Symbolic Computation 
(RISC), Johannes Kepler University Linz, Austria},
  year = {2016},
  month = {May},
  note = {To appear}
}
