Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL

DOI10.1007/978-3-030-23250-4_11MaRDI QIDQ2287906zbMATH OpenOpenAlexFDO

Authors Alexander Maletzky

Publication date 22 January 2020

Full work available at URL https://doi.org/10.1007/978-3-030-23250-4_11

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• New developments in the theory of Gröbner bases and applications to formal verification
• Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• Theorem proving for and with Gröbner bases theory
• Context Aware Calculation and Deduction
• scientific article; zbMATH DE number 589125
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• An Isabelle/HOL formalisation of Green's theorem

Cited in

(5)

• Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Formalising Knot Theory in Isabelle/HOL
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds

Describes a project that uses

Uses Software

• Isabelle/HOL
• Groebner_Bases
• Polynomials
• Isabelle/Isar

This page was built for publication: Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL

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