Note ABES On the formalization of foundations of geometry Sur la formalisation des fondements de la géométrie Formalisation Fondements de la géométrie Formalization Foundations of Geometry 004 516 Géométrie -- Informatique Axiomes Langages formels Dans cette thèse, nous examinons comment un assistant de preuve peut être utilise pour étudier les fondements de la géométrie. Nous débutons en nous concentrant sur les façons d’axiomatiser la géométrie euclidienne et leurs relations. Ensuite, nous exposons une nouvelle preuve de l’indépendance de l’axiome des parallèles des autres axiomes de la géométrie euclidienne du premier ordre. Cela nous amène à affiner la classification des plans de Hilbert de Pejas en considérant les propriétés de décidabilité. Mais, notre intuition nous amène souvent à négliger leur utilisation. Un assistant de preuve nous permet d’utiliser un outil parfait qui ne possède aucune intuition : un ordinateur. De plus, les assistants de preuve nous laissent exploiter les capacités de calcul des ordinateurs. Nous démontrons comment utiliser de méthodes algébriques de déduction automatique en géométrie synthétique. Enfin, nous présentons une procédure spécifique destinée à automatiser des preuves d’incidence. In this thesis, we investigate how a proof assistant can be used to study the foundations of geometry. We start by focusing on ways to axiomatize Euclidean geometry and their relationship to each other. Then, we expose a new proof that Euclid’s parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. This leads us to refine Pejas’ classification of parallel postulates. We do so by considering decidability properties when classifying the postulates. However, our intuition often guides us to overlook uses of such properties. A proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants let us leverage the computational capabilities of computers. We demonstrate how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we present a specific procedure designed to automate proofs of incidence properties. Electronic Thesis or Dissertation Text en PDF 1290818 Université de Strasbourg Strasbourg 2019-12-31 https://theses.hal.science/tel-02166221 application/pdf 1651779 https://publication-theses.unistra.fr/public/theses_doctorat/2018/Boutry_Pierre_2018_ED269.pdf http://www.theses.fr/2018STRAD042/abes https://theses.hal.science/tel-02166221 https://theses.hal.science/tel-02166221 https://theses.hal.science/tel-02166221 Boutry Pierre 1988-12-09 FR 236688456 https://theses.fr/2018STRAD042 2018STRAD042 https://doi.org/10.70675/69a219a5zd6c2z401dz9dd2zfa340fb921e2 2018-11-13 Informatique Strasbourg 131056549 Doctorat Docteur es non oui Schreck Pascal MADS_DIRECTEUR_DE_THESE_1 115931589 Dowek Gilles MADS_PRESIDENT_DU_JURY 02935093X Coquand Thierry MADS_MEMBRE_DU_JURY_1 139931422 Mahboubi Assia MADS_MEMBRE_DU_JURY_2 111289971 Narboux Julien MADS_MEMBRE_DU_JURY_3 111206480 Dowek Gilles MADS_RAPPORTEUR_1 02935093X Janičić Predrag MADS_RAPPORTEUR_2 236688766 École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) MADS_ECOLE_DOCTORALE_1 156504863 Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg ; 2013-....) MADS_PARTENAIRE_DE_RECHERCHE_1 176969721 260728 ddc:004 ddc:510 Schreck Pascal Dowek Gilles Coquand Thierry Mahboubi Assia Narboux Julien Dowek Gilles Janičić Predrag École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg) PDF 1290818