A machine-checked implementation of Buchberger's algorithm
From MaRDI portal
Publication:1595926
DOI10.1023/A:1026518331905zbMath0964.03012OpenAlexW2007116092MaRDI QIDQ1595926
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
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)
Related Items (8)
Commutative algebra in the Mizar system ⋮ Providing a formal linkage between MDG and HOL ⋮ Admissible ordering on monomials is well-founded: a constructive proof ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ Certifying properties of an efficient functional program for computing Gröbner bases ⋮ Mathematical Theory Exploration in Theorema: Reduction Rings ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2
Uses Software
This page was built for publication: A machine-checked implementation of Buchberger's algorithm
