Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL

DOI10.1007/978-3-319-96812-4_16zbMATH Open1417.68189arXiv1805.00304OpenAlexW2810124406MaRDI QIDQ1798967FDOQ1798967

Authors: Alexander Maletzky, Fabian Immler 

Publication date: 18 October 2018

Abstract: We present an elegant, generic and extensive formalization of Gr"obner bases 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 Gr"obner bases. Particular highlights are the first-time formalization of Faug`ere'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) Gr"obner bases and syzygy modules.

Full work available at URL: https://arxiv.org/abs/1805.00304

Recommendations

• A generic and executable formalization of signature-based Gröbner basis algorithms
• Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
• A refinement-based approach to computational algebra in Coq
• Artificial Intelligence and Symbolic Computation
• A verified common lisp implementation of Buchberger's algorithm in ACL2

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Cited In (11)

• A generic and executable formalization of signature-based Gröbner basis algorithms
• A modular first formalisation of combinatorial design theory
• Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
• Certifying properties of an efficient functional program for computing Gröbner bases
• Artificial Intelligence and Symbolic Computation
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Context Aware Calculation and Deduction
• Recurrence-Driven Summations in Automated Deduction
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning

Uses Software

• Isabelle
• Isabelle/HOL
• Mizar
• HOL
• Jordan Normal Forms
• Groebner_Bases
• Deep_Learning
• Polynomials

This page was built for publication: Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1798967)