3 search results - page 1 / 1 » Constructive Reals in Coq: Axioms and Categoricity |
TYPES
2000
Springer
14 years 2 months ago
2000
Springer
We describe a construction of the real numbers carried out in the Coq proof assistant. The basis is a set of axioms for the constructive real numbers as used in the FTA (Fundamenta...
TYPES
2000
Springer
14 years 2 months ago
2000
Springer
Abstract. The aim of this work is to characterize constructive real numbers through a minimal axiomatization. We introduce, discuss and justify 16 constructive axioms. Then we addr...
TYPES
2000
Springer
14 years 2 months ago
2000
Springer
Abstract. In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have first defined the (constructiv...