Skip to Main content Skip to Navigation
Conference papers

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

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

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01228612
Contributor : Julien Narboux <>
Submitted on : Saturday, December 19, 2015 - 9:24:48 AM
Last modification on : Saturday, October 27, 2018 - 1:23:52 AM
Long-term archiving on: : Saturday, April 29, 2017 - 10:21:12 PM

File

jfla2016-gries-boutry-narboux....
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01228612, version 2

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), Jade Algave; Julien Signoles, Jan 2016, Saint Malo, France. pp.15. ⟨hal-01228612v2⟩

Share

Metrics

Record views

389

Files downloads

670