Cerca nel sito
ICube   >   Agenda : Seminaire ITI IRMIA : Julien Narboux : Mechanical verification of proofs in geometry

Seminaire ITI IRMIA : Julien Narboux : Mechanical verification of proofs in geometry

20 ottobre 2022

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)

À la une

Le dépôt des candidatures pour les postes d’enseignants-chercheur est ouvert. Les offres sont...

Flux RSS

Flux RSS