Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq

Charly Gries 1, * Pierre Boutry 1 Julien Narboux 1
* Auteur correspondant
1 ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Résumé : Nous nous intéressons dans cet article au 5e postulat d'Euclide. Ce postulat a une importance historique : pendant des siècles, de nombreux mathématiciens de renom ont cru que cet axiome était un théorème qui pouvait être dérivé des quatre premiers postulats d'Euclide. Dans cet article nous présentons la formalisation en Coq de résultats concernant le lien entre l'unicité de la parallèle et le fait que la somme des angles d'un triangle est égale à deux droits. Nous travaillons en logique intuitionniste dans le contexte de l'axiomatique de Tarski. D'une part nous obtenons la preuve formelle de l'équivalence et d'autre part nous clarifions les propriétés de décidabilité nécessaires pour la preuve. Nous étudions également le lien entre l'axiome d'Aristote et la décidabilité de l'intersection entre deux droites.
Mots-clés : formalisation
Type de document :
Communication dans un congrès
Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint Malo, France. pp.15, 2016, Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016). 〈http://jfla.inria.fr/2016/〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01228612
Contributeur : Julien Narboux <>
Soumis le : samedi 19 décembre 2015 - 09:24:48
Dernière modification le : samedi 27 octobre 2018 - 01:23:52
Document(s) archivé(s) le : samedi 29 avril 2017 - 22:21:12

Fichier

jfla2016-gries-boutry-narboux....
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01228612, version 2

Collections

JFLA2016 | GEOCOQ | INC-CNRS | SITE-ALSACE | INSA-STRASBOURG | INSA-GROUPE

Citation

Charly Gries, Pierre Boutry, Julien Narboux. Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq. Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint Malo, France. pp.15, 2016, Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016). 〈http://jfla.inria.fr/2016/〉. 〈hal-01228612v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

309

Téléchargements de fichiers

374

Contact


archive-ouverte@inria.fr