Projet ANR-07-BLAN-0329 – GALAPAGOS : Géometrie, Algorithmes, Preuves
Programme : Blanc (BLANC) 2007
Année de financement : 2007
Coordinateur du projet : INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE - INRIA (INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE - INRIA)
Partenaires : Inria Centre Paris - Rocquencourt; Université de Poitiers; Université de Strasbourg
Montant : 223000.0 euros
Date de début : 2007
Durée : 36 mois
Résumé : 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