Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Gröbner Bases, Macaulay Matric...


view this post on Zulip Email Gateway (Aug 22 2022 at 20:01):

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: Mar 28 2024 at 20:16 UTC