index.md

title	lang	header-includes
Real closed fields	en	<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>

View the project on GitHub

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.

Documentation

Related publications, if any, are listed below.

• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination doi:10.2168/LMCS-8(1:2)2012
• Construction of real algebraic numbers in Coq doi:10.1007/978-3-642-32347-8_6

Help and contact

• Report issues on GitHub

Authors and contributors

• Cyril Cohen
• Assia Mahboubi