Gröbner Bases of Modules and Faugère’s $$F_4$$F4 Algorithm in Isabelle/HOL

Autor:	Fabian Immler, Alexander Maletzky
Rok vydání:	2018
Předmět:	Mathematical theory Polynomial Reduction (recursion theory) Hilbert's syzygy theorem Mathematics::Commutative Algebra Computer science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION HOL Computer Science::Symbolic Computation Field (mathematics) Data structure Symbolic computation Algorithm
Zdroj:	Lecture Notes in Computer Science ISBN: 9783319968117 CICM
Popis:	We present an elegant, generic and extensive formalization of Grobner bases, an important mathematical theory in the field of computer algebra, in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger’s algorithm, Buchberger’s criteria for avoiding useless pairs), but also includes more advanced features like reduced Grobner bases. Particular highlights are the first-time formalization of Faugere’s matrix-based \(F_4\) algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Grobner bases and syzygy modules.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::3e9ff86a50ba8ee822ba156f5b3441fd https://doi.org/10.1007/978-3-319-96812-4_16 Zobrazit plný text záznamu