Skip to Main content Skip to Navigation
Theses

Formalized algebraic numbers: construction and first-order theory.

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.
Complete list of metadatas

Cited literature [86 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00780446
Contributor : Cyril Cohen <>
Submitted on : Thursday, January 24, 2013 - 3:30:41 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Document(s) archivé(s) le : Saturday, April 1, 2017 - 9:46:21 AM

File

Identifiers

  • 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⟩

Share

Metrics

Record views

880

Files downloads

1377