PhD defense: Pierre BOUTRY
Team: IGG
Title: On the Formalization of Foundations of Geometry
Abstract: Geometry has always had an important role in the evolution of the foundation of mathematics. For example, Euclid introduced the axiomatic method with his Elements. While Euclid's work was considered as a paradigm of rigorous argumentation for over 2000 years, Moritz Pasch pointed out the need for an additional axiom in 1882. Since Automath, the first logical framework designed in 1967, a plethora of proof assistants have been developed, allowing, amongst other things, to avoid such implicit assumptions. 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 independence proof leads us to refine Pejas' classification of parallel postulates. We do so by not only considering continuity axioms, but also decidability properties to determine whether two versions of this postulate are equivalent or not. As Richard J. Trudeau has written, proving the equivalence of different versions of the parallel postulate without assuming decidability properties or continuity axions requires extreme rigor. To help us in this task, a proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants are valuable in the context of geometry in another way: they let us leverage the computational capabilities of computers. In fact, geometry is one of the fields in which automated theorem proving has been very successful. Thus, we present how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we demonstrate how a specific procedure designed to automate proofs of incidence properties allowed us to handle issues arising when assuming a theory such as Tarski's system of geometry.
The jury is comprised of:
The defense will be held on Tuesday, November 13th, at 2:30 pm in the JF Lefevre amphitheater of the Pole API building in Illkirch (building I).
Le dépôt des candidatures pour les postes d’enseignants-chercheur est ouvert. Les offres sont...
Le salon Pollutec est l'événement international de référence des solutions pour l'environnement...
Le salon Pollutec est l'événement international de référence des solutions pour l'environnement...
Haitao Ge, doctorant à l'INSA Strasbourg au sein de l'équipe Génie civil - énergétique (GCE) a...
Dans le cadre du projet Interreg Offensive Science 2PhaseEx, cinq membres de l’équipe ICube/Mécaflu...
Le 13 novembre, le CNRS a réuni les 26 start-up issues de ses laboratoires sous tutelle,...
L'équipe de l'Université de Strasbourg et la délégation Alsace du CNRS se sont brillamment...
Le vendredi 20 septembre a eu lieu la réunion de lancement du projet INTERREG 2PhaseEx, au...
Le projet ENERGETIC a lancé sa première vidéo promotionnelle illustrant les principaux objectifs et...
Paris 27 aout 2024 – ARCHOS annonce que POLADERME, filiale du Startup studio Medtech du groupe...
Les topographes de l’INSA Strasbourg exerçant leurs activités de recherche au sein de l’équipe...