BLANC - Blanc

Géometrie, Algorithmes, Preuves – GALAPAGOS

Résumé de soumission

Dans ce projet, nous voulons étudier l'application d'outils de démonstration - sur ordinateur à deux aspects de la géométrie: la géométrie algorithmique - et le raisonnement à base de constructions géométriques usuelles, commes - les constructions à la règle et au compas. - Nous utiliserons principalement l'outil de démonstration sur ordinateur Coq. - Vis-à-vis de l'algorithmique géométrique, Coq permet la description des - algorithmes et de leurs spécifications dans un langage proche de celui des - mathématiques et les outils d'extraction de Coq permettent d'en dériver - des programmes exécutables pratiquement sans erreur. Vis-à-vis de la - vérification du raisonnement géométrique, Coq permet de proposer des - systèmes d'axiomes définissant les concepts de base, d'expérimenter avec - l'enchaînement de ces axiomes dans la preuve de théorèmes - arbitrairement complexes, et d'étudier la cohérence de ces axiomes - vis-à-vis d'autres présentations de la géométrie (comme la géométrie sur - R^n). - En géométrie algorithmique, nous voulons d'abord mettre en place des - structures de données élémentaires et des opérations abstraites adaptées - pour les algorithmes géométriques. Une structure de donnée importante - est la structure de carte combinatoire, qui permet d'observer et manipuler - les notions topologiques qui apparaissent habituellement dans les données - géométriques, en les séparant bien des notions numériques de position, qui - font l'objet d'une opération de plongement. Une autre approche pour - donner une base abstraite repose sur la notion d'algèbre géométrique, où - les opérations de base d'un algorithme géométrique sont représentées - comme des opérations dans une structure algébrique fixée, qui permet - d'une part de s'affranchir des problèmes de calcul numérique et d'autre - part de décrire des opérations générales de façon indépendante de la - dimension de l'espace géométrique. - En géométrie algorithmique, nous voulons également asseoir nos - expérimentations sur la vérification formelle de plusieurs algorithmes - connus du domaine: les algorithmes d'enveloppes convexes en deux ou - trois dimensions, les algorithmes de triangulation de Delaunay et, de façon - duale, les algorithmes de calculs de diagrammes de Voronoï, et enfin les - algorithmes de calcul d'arrangements. Dans chaque cas, nous voulons faire - des études préliminaires en dimension 2 puis prolonger nos études à la - troisième dimension, ou quand ce sera possible trouver des formulations - indépendantes de la dimension. - En formalisation du raisonnement géométrique, nous voulons traiter les - constructions usuelles de la géométrie: construire une droite, un cercle, - prendre l'intersection de deux figures, etcetera. Plusieurs approches sont - possibles autour de ces constructions et nous voulons étudier comment ces - différentes approches peuvent être réconciliées. Une première approche - consiste en la description formelle des axiomes de la géométrie tels qu'ils - ont été proposés tout au long de l'histoire des mathématiques. Pour cette - approche, nous nous concentrerons sur les axiomes proposés par Hilbert. - Une deuxième approche consiste à mettre au point un nouveau jeu - d'axiomes plus adapté pour la vérification formelle à l'aide d'un outil de - démonstration sur ordinateur et étendre ce jeu d'axiome pour couvrir des - domaines de plus en plus large de la géométrie. Par cette approche nous - comptons étendre nos travaux antérieurs sur la géométrie planaire pour y - intégrer les raisonnements sur les notions d'incidence, d'aires, d'angles, et - d'inversion. Nous comptons également aborder des concepts de géométrie - tri-dimensionnelle. - En formalisation du raisonnement géométrique, nous voulons égalementréduire le caractère fastidieux des preuves en vérifiant formellement les - méthodes qui permettent d'encoder les problèmes géométriques comme - des problèmes algébriques et de résoudre cert

Coordination du projet

Yves BERTOT (Organisme de recherche)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Aide de l'ANR 223 000 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter