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.
