hal-00671809, version 2
Construction of real algebraic numbers in Coq
Cyril Cohen
1, 2, 3
ITP - 3rd International Conference on Interactive Theorem Proving - 2012 (2012)
Résumé : This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.
- 1 : Microsoft Research - Inria Joint Centre (MSR - INRIA)
- INRIA – Microsoft – Microsoft Research Laboratory Cambridge
- 2 : TYPICAL (INRIA Saclay - Ile de France)
- INRIA – CNRS : UMR – Polytechnique - X
- 3 : Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- Domaine : Informatique/Autre
- Mots-clés : coq – real algebraic numbers – formalization of mathematics – quotient – real closure – small scale reflexion
- Versions disponibles : v1 (19-02-2012) v2 (14-06-2012)
- hal-00671809, version 2
- http://hal.inria.fr/hal-00671809
- oai:hal.inria.fr:hal-00671809
- Contributeur : Cyril Cohen
- Soumis le : Mercredi 13 Juin 2012, 23:24:43
- Dernière modification le : Jeudi 14 Juin 2012, 11:24:29
Documents associés
Exporter