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).
Offers are available in the Job opportunities section of the ICube website or by clicking on the...
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...
Paris 27 aout 2024 – ARCHOS annonce que POLADERME, filiale du Startup studio Medtech du groupe...
La 11e journée du département de mécanique s'est tenue le 18 juin 2024. Lors de cette...
A l'occasion de la soirée de gala du 103ème congrès de l’association française des professionnels...
Le 32ème Congrès Français de Thermique de la Société française de thermique (SFT) organisé par le...
L'un des 3 Prix du meilleur poster de la 11èmes journées de la Fédération de Médecine...
La neurostimulation guidée par l’imagerie cérébrale pour traiter les patients atteints d’épilepsie...
L'un des 3 Prix du meilleur poster de la 11èmes journées de la Fédération de Médecine...
L'AABC Europe (Advanced Automotive Battery Conference) est un événement annuel rassemblant des...