A verified common lisp implementation of Buchberger's algorithm in ACL2

DOI10.1016/J.JSC.2009.07.002MaRDI QIDQ1034553zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

computer algebraformal verificationBuchberger's algorithmACL2

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Abstract data types; algebraic specification (68Q65)

Recommendations

• Artificial Intelligence and Symbolic Computation
• Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
• Computer Aided Systems Theory – EUROCAST 2005
• scientific article; zbMATH DE number 1303350
• A generic and executable formalization of signature-based Gröbner basis algorithms

Cites work

• scientific article; zbMATH DE number 2177625 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• scientific article; zbMATH DE number 108109 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 1120551 (Why is no real title available?)
• scientific article; zbMATH DE number 1420784 (Why is no real title available?)
• A formal proof of Dickson's lemma in ACL2
• A machine-checked implementation of Buchberger's algorithm
• Algorithm synthesis by lazy thinking: using problem schemes
• 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
• Certifying properties of an efficient functional program for computing Gröbner bases
• Commutative algebra in the Mizar system
• Efficient execution in an automated reasoning environment
• Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
• Formal proofs about rewriting using ACL2
• Mathematical Knowledge Management
• Structured theory development for a mechanized logic
• \textit{Theorema}: Towards computer-aided mathematical theory exploration

Cited in

(9)

• Proof assistant decision procedures for formalizing origami
• 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₄ algorithm in Isabelle/HOL
• Artificial Intelligence and Symbolic Computation
• Modelling algebraic structures and morphisms in ACL2
• Computer Aided Systems Theory – EUROCAST 2005

Describes a project that uses

Uses Software

• NQTHM
• LISP
• Mizar
• Theorema
• ACL2

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)