A verified common lisp implementation of Buchberger's algorithm in ACL2
From MaRDI portal
Publication:1034553
DOI10.1016/j.jsc.2009.07.002zbMath1194.68155OpenAlexW2004470082WikidataQ57834883 ScholiaQ57834883MaRDI QIDQ1034553
Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José Luis Ruiz-Reina
Publication date: 6 November 2009
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2009.07.002
Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Abstract data types; algebraic specification (68Q65)
Related Items
Formalization of a normalization theorem in simplicial topology ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ Proof Assistant Decision Procedures for Formalizing Origami ⋮ Mathematical Theory Exploration in Theorema: Reduction Rings ⋮ Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
Cites Work
- Commutative algebra in the Mizar system
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Certifying properties of an efficient functional program for computing Gröbner bases
- A machine-checked implementation of Buchberger's algorithm
- Structured theory development for a mechanized logic
- Formal proofs about rewriting using ACL2
- 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
- Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
- Efficient execution in an automated reasoning environment
- Mathematical Knowledge Management
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
