scientific article; zbMATH DE number 1420784

MaRDI QIDQ4944848zbMATH OpenFDO

Authors Thierry Coquand, Henrik Persson

Publication date 17 February 2002

zbMATH Keywords

constructive type theoryDickson's lemmaGröbner basisHilbert basis theoreminductive definitionspolynomials

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35) Other constructive mathematics (03F65) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Recommendations

• Theorem proving for and with Gröbner bases theory
• scientific article; zbMATH DE number 4112737
• Gröbner bases and systems theory
• Homotopy-initial algebras in type theory
• The theory of Gröbner bases
• Towards Constructive Homological Algebra in Type Theory
• Type theory and homotopy
• Homotopy type theory and Voevodsky's univalent foundations
• scientific article; zbMATH DE number 1302059
• Homotopy type theory

Cited in

(27)

• A verified common lisp implementation of Buchberger's algorithm in ACL2
• Standard bases for general coefficient rings and a new constructive proof of Hilbert's basis theorem
• Strongly Noetherian rings and constructive ideal theory
• A universal Krull-Lindenbaum theorem
• Homotopy type theory and Voevodsky's univalent foundations
• Noetherian orders
• scientific article; zbMATH DE number 5994829 (Why is no real title available?)
• Galois Connections for Recursive Types
• Lindenbaum's lemma via open induction
• A formal proof of Dickson's lemma in ACL2
• scientific article; zbMATH DE number 1163435 (Why is no real title available?)
• Syntax for semantics: Krull's maximal ideal theorem
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Commutative algebra in the Mizar system
• Admissible ordering on monomials is well-founded: a constructive proof
• A constructive picture of Noetherian conditions and well quasi-orders
• A general constructive form of Higman's lemma
• An iterative constructive Hilbert basis theorem
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively

Describes a project that uses

Uses Software

• Agda

This page was built for publication:

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