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
|
---
title: Real closed fields
lang: en
header-includes:
- |
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
<style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
---
<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
<a href="https://github.com/math-comp/real-closed">View the project on GitHub</a>
<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
## About
Welcome to the Real closed fields project website!
This library contains definitions and theorems about real closed
fields, with a construction of the real closure and the algebraic
closure (including a proof of the fundamental theorem of
algebra). It also contains a proof of decidability of the first
order theory of real closed field, through quantifier elimination.
This is an open source project, licensed under the CeCILL-B.
## Get the code
The current stable release of Real closed fields can be [downloaded from GitHub](https://github.com/math-comp/real-closed/releases).
## Documentation
Related publications, if any, are listed below.
- [Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination](https://hal.inria.fr/inria-00593738v4) doi:[10.2168/LMCS-8(1:2)2012](https://doi.org/10.2168/LMCS-8(1:2)2012)
- [Construction of real algebraic numbers in Coq](https://hal.inria.fr/hal-00671809v2) doi:[10.1007/978-3-642-32347-8_6](https://doi.org/10.1007/978-3-642-32347-8_6)
## Help and contact
- Report issues on [GitHub](https://github.com/math-comp/real-closed/issues)
## Authors and contributors
- Cyril Cohen
- Assia Mahboubi
|
