Résumé : Afin de pouvoir démontrer formellement la correction d'algorithmes géométriques en Coq, il est nécessaire de disposer d'outils pour automatiser au moins partiellement les démonstrations en géométrie. Nous étudions cette question dans le cadre simple de la géométrie projective en utilisant une approche combinatoire et la notion de rang d'un ensemble de points. L'outil proposé, implanté en C, procède par saturation du contexte et permet de démontrer automatiquement de nombreux théorèmes emblématiques de la géométrie projective. Afin de s'assurer de la correction de ces démonstrations, l'outil produit une trace sous la forme d'un script de preuve, qui est ensuite vérifié par Coq.
Bio : Nicolas Magaud a effectué sa thèse dans le domaine des preuves formelles avec l’assistant de preuves Coq (INRIA Sophia-Antipolis, 2003). Il a ensuite été chercheur post-doctorant à Sydney (2003-2005), où il a travaillé sur la certification de code fonctionnel en théorie des types avec LF. Depuis son recrutement comme maître de conférences à l’Université de Strasbourg en 2005, il s’attache à adapter les outils de preuves formelles comme Coq à la modélisation des résultats géométriques. Son habilitation, soutenue en 2020, synthétise ses contributions, notamment en géométrie algorithmique (preuves formelles d’algorithmes géométriques), en démonstration automatique (preuves automatiques de propriétés en géométrie projective 3D et plus), et en calcul réel exact.
