A logical approach to abstract algebra

DOI10.1017/S0960129506005627zbMath1118.03059MaRDI QIDQ3422024

Thierry Coquand, Henri Lombardi

Publication date: 9 February 2007

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

commutative rings; constructive algebra; positive formula; geometric formula

Mathematics Subject Classification ID

13C10: Projective and free modules and ideals in commutative rings

13L05: Applications of logic to commutative algebra

03F65: Other constructive mathematics

Related Items

Un anneau de Prüfer, Syntax for Semantics: Krull’s Maximal Ideal Theorem, THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY, Spectral Spaces Versus Distributive Lattices: A Dictionary, ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION, Constructing Gröbner bases for Noetherian rings, Maximal elements with minimal logic, Valuative Lattices and Spectra, Valuative dimension, constructive points of view, A universal Krull-Lindenbaum theorem, A formal proof of the projective Eisenbud-Evans-Storch theorem, Constructive finite free resolutions, The basic Zariski topology, A mechanized proof of the basic perturbation lemma, Space of valuations, Eliminating disjunctions by disjunction elimination, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Towards formal Baer criteria, Maximal ideals in countable rings, constructively, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Cut elimination for entailment relations, Spectral schemes as ringed lattices, A constructive notion of codimension, A universal algorithm for Krull's theorem, Noetherian orders, On the Constructive and Computational Content of Abstract Mathematics, On some peculiar aspects of the constructive theory of point-free spaces