scientific article; zbMATH DE number 1420784
From MaRDI portal
Publication:4944848
zbMath0979.03044MaRDI QIDQ4944848
Thierry Coquand, Henrik Persson
Publication date: 17 February 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Gröbner basispolynomialsDickson's lemmaconstructive type theoryinductive definitionsHilbert basis theorem
Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65) Second- and higher-order arithmetic and fragments (03F35)
Related Items (8)
A universal Krull-Lindenbaum theorem ⋮ Commutative algebra in the Mizar system ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Admissible ordering on monomials is well-founded: a constructive proof ⋮ A constructive picture of Noetherian conditions and well quasi-orders ⋮ Lindenbaum’s Lemma via Open Induction ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2 ⋮ Syntax for Semantics: Krull’s Maximal Ideal Theorem
Uses Software
This page was built for publication: