From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
the following new entry is available in the AFP.
Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
by Alexander Maletzky
This entry formalizes the connection between Gröbner bases and Macaulay matrices
(sometimes also referred to as `generalized Sylvester matrices'). In particular,
it contains a method for computing Gröbner bases, which proceeds by first
constructing some Macaulay matrix of the initial set of polynomials, then
row-reducing this matrix, and finally converting the result back into a set of
polynomials. The output is shown to be a Gröbner basis if the Macaulay matrix
constructed in the first step is sufficiently large. In order to obtain concrete
upper bounds on the size of the matrix (and hence turn the method into an
effectively executable algorithm), Dubé's degree bounds on Gröbner bases are
utilized; consequently, they are also part of the formalization.
https://www.isa-afp.org/entries/Groebner_Macaulay.html
Enjoy,
René
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC