The next seminar of our Interdisciplinary Thematic Institute (ITI) IRMIA++ will be held this Thursday October 20th at 09:00 am, both in the IRMA conference room and on BBB.
The talk will be given by: Julien NARBOUX (ICube).
Title: Mechanical verification of proofs in geometry
BBB link: https://bbb.unistra.fr/b/hum-51d-suf-mzq
Abstract: The first part will consist of a short introduction to the field of computer verified proofs. Why verify proofs with a computer? what can be verified? what are the challenges? In a second part, I will give an overview of our formalizations concerning the foundations of geometry based on the axiom systems of Hilbert, Tarski and Euclid. In particular, I will present a joint work with Michael Beeson and Freek Wiedijk which consisted in mechanically verifying the proofs of the first book of Euclid's Elements while trying to stay as close as possible to the original proofs. I will discuss the classification of 34 versions of the axioms of parallels (joint work with Pierre Boutry). We will finish by presenting a syntactic proof of the independence of the axiom of parallels (joint work with Michael Beeson and Pierre Boutry).
Bio: Julien Narboux is Maître de Conférences at the Université de Strasbourg, and pursues his research at ICube (IGG team).
His research interests include formal proofs and formalisation of foundations of geometry and applications.
He is especially interested in automated reasoning (in particular in geometry) and using proof assistants for teaching.
Next seminar: November 24, 2022 at 09:00 am : Pierre Ocvirk (ObAS)
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...