Formalized algebraic numbers: construction and first-order theory.

Cyril Cohen 1, 2, 3, 4
3 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.
Type de document :
Thèse
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English
Liste complète des métadonnées

https://pastel.archives-ouvertes.fr/pastel-00780446
Contributeur : Cyril Cohen <>
Soumis le : jeudi 24 janvier 2013 - 03:30:41
Dernière modification le : jeudi 9 février 2017 - 15:16:52

Fichier

Identifiants

  • HAL Id : pastel-00780446, version 1

Collections

Citation

Cyril Cohen. Formalized algebraic numbers: construction and first-order theory.. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2012. English. <pastel-00780446>

Partager

Métriques

Consultations de
la notice

490

Téléchargements du document

621