Email Gateway (Aug 22 2022 at 18:17): Email Gateway (Aug 22 2022 at 18:17):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
the AFP now contains a new efficient algorithm to compute Gröbner bases.
Signature-Based Gröbner Basis Algorithms
by Alexander Maletzky
This article formalizes signature-based algorithms for computing Gröbner bases.
Such algorithms are, in general, superior to other algorithms in terms of
efficiency, and have not been formalized in any proof assistant so far. The
present development is both generic, in the sense that most known variants of
signature-based algorithms are covered by it, and effectively executable on
concrete input thanks to Isabelle's code generator. Sample computations of
benchmark problems show that the verified implementation of signature-based
algorithms indeed outperforms the existing implementation of Buchberger's
algorithm in Isabelle/HOL.
Besides total correctness of the algorithms, the article also proves that under
certain conditions they a-priori detect and avoid all useless zero-reductions,
and always return 'minimal' (in some sense) Gröbner bases if an input parameter
is chosen in the right way.
The formalization follows the recent survey article by Eder and Faugère.
More details at: https://www.isa-afp.org/entries/Signature_Groebner.html
Many thanks to Alexander,
René
Email Gateway (Aug 22 2022 at 18:18):From: Tobias Nipkow <nipkow@in.tum.de>
I would like to add that with this new article the size of the AFP has crossed
the 2 million LOC mark and contains 2,002,100 LOC now.
Thanks to all the contributors and maintainers.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC