Preuves en géométrie
Cursus master ingénierie (CMI)Parcours Cursus master ingénierie (CMI) - Informatique, image, réalité virtuelle, interactions et jeux
ComposanteUFR de mathématique et d'informatique
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 M1Compé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ïdesBibliographie
- Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s Elements. Rev. Symbolic Logic 2(4), 700–768 (2009)