Search & Find
Vous êtes ici :  UFR Mathématique-Informatique   >   Bienvenue   >   Offre de formation

Master de sciences, mention Informatique
Spécialité : Informatique et sciences de l'image (M2 en alternance et en apprentissage)

Semestre S3 > 'Constructions et preuves en géométrie'

Pré-requis

M1 Informatique (ou équivalent)

Contenu

Preuves et certification en géométrie
Spécifications et preuves en géométrie. Axiomatiques de la géométrie (Euclide, Hilbert, Tarski) ; Théorème de Tarski sur la décidabilité de la géométrie ; Spécification en calcul des constructions inductives de la topologie combinatoire, de la géométrie, et des algorithmes associés. Preuves assistées avec le système Coq. Construction et certification d'algorithmes topologiques et géométriques. Exemples de la formule d'Euler, du théorème de Jordan, de la segmentation d'images ; Preuves en géométrie pure axiomatisée et méthode de vérification sémantique (Gelernter, Bundy). Méthode des aires de Chou, Gao et Zhang ; Preuves fondées sur l'algèbre polynomiale. Idéaux de polynômes, méthode de Wu, bases de Gröbner, décomposition cylindrique. Étude du prouveur de Chou. Algorithme de Fourier-Motzkin pour la résolution d'inéquations linéaires dans les réels.
Résolution de Contraintes Géométriques
Introduction à la résolution de contraintes géométriques, point de vue constructif vs point de vue CAO. Définitions générales : système de contraintes, syntaxe et sémantique, constriction, invariance par un groupe de transformations. Constructions à la règle et au compas, rappels d'algèbres, résultat de Wantzel et méthode de Lebesgue (utilisant, par exemple, la pseudo-division de Wu ou les bases de Gröbner). Méthodes numériques générales : Newton-Raphson, méthodes par continuation, arithmétique des intervalles. Décomposition de systèmes de contraintes : couplages, couplages maximaux et parfaits, méthodes à base de flux. Théorie de la rigidité. Méthodes de rigidification progressive : systèmes à base de connaissance, propagation des degrés liberté, utilisation de l'invariance par des groupes, repères, clusters, bords et assemblage.

Objectifs : savoir-faire et compétences

- Acquérir les bases nécessaires à un travail de recherche ou de développement en preuves et constructions géométriques assistées par ordinateur
- Mobiliser des techniques de raisonnement relevant de l'ingénierie du logiciel et de l'intelligence artifcielle dans un domaine concret et attrayant
- Définir et concevoir des modules de programmes intelligents pour des systèmes de CAO et d'EIAO.

Autres informations

Evaluation continuée intégrale :
Contrôle continu

Volume horaire
Cours : 26h