A verified common lisp implementation of Buchberger's algorithm in ACL2
DOI10.1016/J.JSC.2009.07.002zbMATH Open1194.68155OpenAlexW2004470082WikidataQ57834883 ScholiaQ57834883MaRDI QIDQ1034553FDOQ1034553
Authors: 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
Recommendations
Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Structured theory development for a mechanized logic
- Title not available (Why is that?)
- Commutative algebra in the Mizar system
- Title not available (Why is that?)
- Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
- A formal proof of Dickson's lemma in ACL2
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Title not available (Why is that?)
- Algorithm synthesis by lazy thinking: using problem schemes
- A machine-checked implementation of Buchberger's algorithm
- Formal proofs about rewriting using ACL2
- Title not available (Why is that?)
- Efficient execution in an automated reasoning environment
- Certifying properties of an efficient functional program for computing Gröbner bases
- Mathematical Knowledge Management
Cited In (9)
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Mathematical theory exploration in Theorema: reduction rings
- Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
- Formalization of a normalization theorem in simplicial topology
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
- Artificial Intelligence and Symbolic Computation
- Modelling algebraic structures and morphisms in ACL2
- Computer Aided Systems Theory – EUROCAST 2005
- Proof assistant decision procedures for formalizing origami
Uses Software
This page was built for publication: A verified common lisp implementation of Buchberger's algorithm in ACL2
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1034553)
