Equipe de recherche LOGICAL

Logique et Calcul

Présentation de l'équipe

Le but des recherches menées dans l'équipe-projet est de construire des systèmes de traitement de démonstrations mathématiques, c'est à dire des systèmes capables d'opérer des traitements divers sur des connaissances mathématiques. Ces systèmes peuvent vérifier l'absence d'erreurs dans une démonstration, ils peuvent aider les utilisateurs à construire des démonstrations interactivement, en rechercher de manière automatique, les archiver, les transmettre sur les réseaux, ...

Utiliser un système informatique pour traiter des démonstrations mathématiques permet de se convaincre avec un grand degré de certitude que ces démonstrations ne comportent pas d'erreurs. On peut, en particulier se convaincre ainsi de l'exactitude des arguments justifiant la correction de matériels et de logiciels. Cela est particulièrement important dans les domaines applicatifs où un défaut de fonctionnement met la vie humaine, la santé ou l'environnement en péril et dans celles qui mettent en jeu des sommes d'argent importantes : l'informatique médicale, les transports, les télécomunications, le commerce électronique, l'informatique en réseau, ...

Utiliser un système de traitement de démonstrations permet également de construire des démonstrations de grande taille, par exemple des démonstrations utilisant des polynômes formés de plusieurs centaines de monômes. Enfin, cela participe à la quête d'une nouvelle forme d'exactitude et de rigueur dans la rédaction mathématique : le point où rien n'est sous-entendu, et où le lecteur peut donc être remplacé par un programme.
Le principal axe de nos travaux est le développement du système Coq qui a aujourd'hui une communauté importante d'utilisateurs industriels et académiques. Nous croyons cependant que le développement d'un système ne peut pas s'effectuer sans une réflexion en aval sur les usages spécifiques que l'on fait de ce système dans certains domaines (quand on fait de la géométrie réelle, des preuves de programmes impératifs ou objets, des preuves de protocoles cryptographiques, ...) et en amont sur les questions relatives à la formalisation des mathématiques (sur la représentation des démonstrations, sur l'intégration d'un langage de programmation dans un formalisme mathématique, sur la notion de variable liée, ...). Ces recherches s'articulent autour de deux notions clés : celle de raisonnement logique et celle de calcul. Ce sont ces deux notions qui donnent son nom à l'équipe-projet LOGICAL.

Axes de recherche

Le premier axe de recherche de l'équipe-projet est le développement du système Coq en particulier de nouvelles fonctionnalités tels les modules, les définitions par filtrage, les structures de données infinies, les langages de tactiques ou la réduction rapide des termes exprimant les démonstrations.
Un autre axe de recherche concerne la théorie de la démonstration, en particulier l'étude des formalismes intégrant le calcul a` la déduction, les algorithmes de réduction des démonstrations, et les algorithmes de recherche de démonstrations.
Un troisième axe est le développement de théories mathématiques dans le système Coq, en particulier en géométrie réelle, en théorie des graphes et en logique.