| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [23 references]
https://hal.inria.fr/hal-01228612
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Saturday, December 19, 2015 - 9:24:48 AM
Last modification on : Thursday, December 2, 2021 - 3:16:49 AM
Long-term archiving on: : Saturday, April 29, 2017 - 10:21:12 PM
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Saturday, December 19, 2015 - 9:24:48 AM
Last modification on : Thursday, December 2, 2021 - 3:16:49 AM
Long-term archiving on: : Saturday, April 29, 2017 - 10:21:12 PM
File
jfla2016-gries-boutry-narboux....
Files produced by the author(s)