Complexity Analysis
Keywords 
Buchberger's algorithm, complexity analysis, Gröbner bases 
Put online 
April 22, 2016 
Size 
20.1 MB (zipped), 115.0 MB (unzipped) 
SubTheories (1) 
Complexity (no functor)

Depends on 
 
Download 
Complexity Analysis.zip 
Abstract
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. ComputerAssisted 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 59).
LNCS 8592, pages 4148, Springer, 2014.
doi:10.1007/9783662441992_8
Literature on the Underlying Theory

B. Buchberger. A Note on the Complexity of Constructing GröbnerBases.
In J. A. van Hulzen, editor, Computer Algebra (Proceedings of EUROCAL 1983, London, England, March 2830).
LNCS 162, pages 137145, Springer, 1983.
doi:10.1007/3540128689_98

B. Buchberger. Miscellaneous Results on the GröbnerBases for Polynomial Ideals II.
Technical report 831, Department of Computer And Information Sciences, University of Delaware, 1983.

B. Buchberger and F. Winkler. Miscellaneous Results on the Construction of GröbnerBases for Polynomial Ideals.
Technical report 137, Institut für Mathematik, JKU Linz, 1979.