forked from coq-community/corn
-
Notifications
You must be signed in to change notification settings - Fork 0
/
description
65 lines (56 loc) · 2.01 KB
/
description
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
Name: CoRN
Title: Constructive Coq Repository at Nijmegen
Author: Herman Geuvers
Institution: Radboud University Nijmegen
Author: Luís Cruz-Filipe
Institution: Radboud University Nijmegen
Author: Milad Niqui
Institution: Radboud University Nijmegen
Author: Freek Wiedijk
Institution: Radboud University Nijmegen
Author: Jan Zwanenburg
Institution: Radboud University Nijmegen
Author: Randy Pollack
Author: Henk Barendregt
Institution: Radboud University Nijmegen
Author: Mariusz Giero
Author: Rik van Ginneken
Institution: Radboud University Nijmegen
Author: Dimitri Hendriks
Author: Sébastien Hinderer
Author: Bart Kirkels
Author: Pierre Letouzey
Author: Iris Loeb
Institution: Radboud University Nijmegen
Author: Lionel Mamane
Author: Russell O'Connor
Institution: Radboud University Nijmegen
Author: Nickolay V. Shmyrev
Author: Bas Spitters
Institution: Radboud University Nijmegen
Author: Dan Synek
Institution: Radboud University Nijmegen
Description:
The Constructive Coq Repository at Nijmegen, C-CoRN, aims at building
a computer based library of constructive mathematics, formalized in
the theorem prover Coq. It includes the following parts:
* Algebraic Hierarchy
o An axiomatic formalization of the most common algebraic
structures, including setoids, monoids, groups, rings,
fields, ordered fields, rings of polynomials, real and
complex numbers
* Model of the Real Numbers
o Construction of a concrete real number structure
satisfying the previously defined axioms
* Fundamental Theorem of Algebra
o A proof that every non-constant polynomial on the complex
plane has at least one root
* Real Calculus
o A collection of elementary results on real analysis,
including continuity, differentiability, integration,
Taylor's theorem and the Fundamental Theorem of Calculus
URL: http://c-corn.cs.ru.nl
Keywords: constructive mathematics, algebra, real calculus, real numbers,
Fundamental Theorem of Algebra
Category: Mathematics/Algebra
Category: Mathematics/Real Calculus and Topology