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

DOI10.1007/978-3-319-96812-4_16MaRDI QIDQ1798967zbMATH OpenOpenAlexFDO

Authors Alexander Maletzky, Fabian Immler

Publication date 18 October 2018

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

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)

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.

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

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
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• 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

Describes a project that uses

Uses Software

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

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)