A generic and executable formalization of signature-based Gröbner basis algorithms
From MaRDI portal
Publication:2028994
DOI10.1016/j.jsc.2020.12.001zbMath1467.13050arXiv2012.02239OpenAlexW3113373060MaRDI QIDQ2028994
Publication date: 3 June 2021
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2012.02239
Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- HOL
- F5C: A variant of Faugère's F5 algorithm with reduced Gröbner bases
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Certifying properties of an efficient functional program for computing Gröbner bases
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- A new efficient algorithm for computing Gröbner bases \((F_4)\)
- Isabelle. A generic theorem prover
- A machine-checked implementation of Buchberger's algorithm
- Isabelle/HOL. A proof assistant for higher-order logic
- A survey on signature-based algorithms for computing Gröbner bases
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
- Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
- Signature rewriting in gröbner basis computation
- Mizar: State-of-the-art and Beyond
- Theorema 2.0: Computer-Assisted Natural-Style Mathematics
- Practical Gröbner basis computation
- Data Refinement in Isabelle/HOL
- Context Aware Calculation and Deduction
- Mathematical Knowledge Management
This page was built for publication: A generic and executable formalization of signature-based Gröbner basis algorithms
