Description

La spécialité I3D fait un grand usage de la géométrie que ce soit dans la définition de types abstraits en modélisation ou dans la conception des algorithmes dans les domaines ayant trait à l'image ou la réalité virtuelle. L'objectif de cette UE est de bien comprendre les fondements de la géométrie synthétique en lien avec la géométrie analytique et de réfléchir à la correction des méthodes utilisées dans les autres matières géométriques.

Compétences requises

Logique, Preuve assistée par ordinateur et les UE de géométrie de M1

Compétences visées

• connaître les différentes manières de décrire formellement la géométrie de manière synthétique
• savoir utiliser la méthodes des aires
• comprendre l’approche combinatoire pour la preuve automatique en géométrie d’incidence: matroïdes et rang
• étudier les espaces projectifs finis et leurs propriétés combinatoires
• prendre en main les bibliothèques formelles en Coq sur la géométrie

Disciplines

• Informatique

Syllabus

On s’intéressera principalement à la preuve en géométrie avec la présentation des fondements et différentes méthodes de preuves automatiques.  Le cœur de cet enseignement portera sur la formalisation de la géométrie au moyen de l’assistant de preuves Coq. Il comportera une introduction à la librairie GeoCoq, la présentation de méthodes de preuves automatiques comme la méthode des aires, la méthode de Wu, ou des approches combinatoires basées sur la théorie des matroïdes

Bibliographie

• Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symbolic Logic 2(4), 700–768 (2009)