This formalization is concerned with the complexity analysis of Buchberger's algorithm in the case of bivariate polynomial
rings over fields, if a graded term order is used.
In more concrete terms, the main results in this formalization are about certain bounds on the degrees of the polynomials
in the Gröbner basis computed by Buchberger's algorithm with chain criterion, expressed in terms of the degrees of
the polynomials in the original input set. Knowing such bounds it is comparatively easy to come up with good estimates
about the total number of elementary operations that actually have to be carried in the course of the algorithm; this latter
calculation, however, is not included in the present formalization.
Literature
Literature on the Formalization
A. Maletzky. Computer-Assisted Exploration of Gröbner Bases Theory in Theorema. PhD thesis, RISC, JKU Linz, May 2016.
[pdf]
A. Maletzky and B. Buchberger. Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema.
In H. Hong and C. Yap, editors,
Mathematical Software (Proceedings of ICMS 2014, Seoul, Korea, August 5-9).
LNCS 8592, pages 41-48, Springer, 2014.
doi:10.1007/978-3-662-44199-2_8
Literature on the Underlying Theory
B. Buchberger. A Note on the Complexity of Constructing Gröbner-Bases.
In J. A. van Hulzen, editor, Computer Algebra (Proceedings of EUROCAL 1983, London, England, March 28-30).
LNCS 162, pages 137-145, Springer, 1983.
doi:10.1007/3-540-12868-9_98
B. Buchberger. Miscellaneous Results on the Gröbner-Bases for Polynomial Ideals II.
Technical report 83-1, Department of Computer And Information Sciences, University of Delaware, 1983.
B. Buchberger and F. Winkler. Miscellaneous Results on the Construction of Gröbner-Bases for Polynomial Ideals.
Technical report 137, Institut für Mathematik, JKU Linz, 1979.
