A machine-checked implementation of Buchberger's algorithm

DOI10.1023/A:1026518331905MaRDI QIDQ1595926zbMATH OpenOpenAlexFDO

Authors Laurent Théry

Publication date 18 February 2001

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1026518331905

zbMATH Keywords

computer algebraGröbner basesprogram verificationtheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Symbolic computation and algebraic computation (68W30)

Cited in

(12)

• Certifying properties of an efficient functional program for computing Gröbner bases
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Mathematical theory exploration in Theorema: reduction rings
• Constructive Formalization of Hybrid Logic with Eventualities
• scientific article; zbMATH DE number 1303350 (Why is no real title available?)
• scientific article; zbMATH DE number 782043 (Why is no real title available?)
• scientific article; zbMATH DE number 915924 (Why is no real title available?)
• A Mechanically Verified AIG-to-BDD Conversion Algorithm
• Commutative algebra in the Mizar system
• Admissible ordering on monomials is well-founded: a constructive proof
• Providing a formal linkage between MDG and HOL

Describes a project that uses

Uses Software

• Coq
• Theorema
• Mizar
• Nuprl

This page was built for publication: A machine-checked implementation of Buchberger's algorithm

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