Preuves et résolution de contraintes géométriques

Preuves et résolution de contraintes géométriques
DU - Mathématiques & InformatiqueParcours Mathématiques et applications : recherche et interactions

Credits3 crédits

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.
Pour cela, deux grands domaines sont explorés : d'une part, la preuve en géométrie avec la présentation des fondements et différentes méthodes de preuves automatiques ; et d'autre part, la gestion des contraintes géométriques comme méthode de spécification de scènes et de figures. Ces deux domaines sont intimement liés même s'ils donnent lieu à des applications différentes. Ainsi, la résolution de contraintes géométriques trouve naturellement des applications en CAO avec la modélisation paramétrique, et les preuves en géométrie constituent un ingrédient essentiel de la certification des logiciels produits en géométrie algorithmique.
Parmi les points qui seront étudiés pour illustrer cette matière, il pourra y avoir :
la formalisation de la géométrie et la prise en main de la librairie GeoCoq,
la présentation de méthodes de preuves automatiques comme la méthode des aires et la méthode de Wu,
la théorie de construction à la règle et au compas et les implantations de solveur s'appuyant sur des systèmes à base de connaissances,
les techniques de décomposition, notamment celles à base de graphe, en distinguant celles qui prennent en compte l'invariance par déplacement,
les méthodes numériques générales usuelles, comme les méthodes fondées sur la méthode de Newton-Raphson ou les méthodes par continuation, et leur adaptation à la géométrie.

Compétences visées

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.
Pour cela, deux grands domaines sont explorés : d'une part, la preuve en géométrie avec la présentation des fondements et différentes méthodes de preuves automatiques ; et d'autre part, la gestion des contraintes géométriques comme méthode de spécification de scènes et de figures. Ces deux domaines sont intimement liés même s'ils donnent lieu à des applications différentes. Ainsi, la résolution de contraintes géométriques trouve naturellement des applications en CAO avec la modélisation paramétrique, et les preuves en géométrie constituent un ingrédient essentiel de la certification des logiciels produits en géométrie algorithmique.
Parmi les points qui seront étudiés pour illustrer cette matière, il pourra y avoir :
la formalisation de la géométrie et la prise en main de la librairie GeoCoq,
la présentation de méthodes de preuves automatiques comme la méthode des aires et la méthode de Wu,
la théorie de construction à la règle et au compas et les implantations de solveur s'appuyant sur des systèmes à base de connaissances,
les techniques de décomposition, notamment celles à base de graphe, en distinguant celles qui prennent en compte l'invariance par déplacement,
les méthodes numériques générales usuelles, comme les méthodes fondées sur la méthode de Newton-Raphson ou les méthodes par continuation, et leur adaptation à la géométrie.