s'authentifier
version française rss feed

hal-00671809, version 2

Construction of real algebraic numbers in Coq

Cyril Cohen () 123

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.

  • 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
  • oai:hal.inria.fr:hal-00671809
  • Contributeur : 
  • Soumis le : Mercredi 13 Juin 2012, 23:24:43
  • Dernière modification le : Jeudi 14 Juin 2012, 11:24:29
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...