Loading...
 
[Show/Hide Left Column]

UPSCaLe : Universality of Proofs in SaCLay

 

Axe : SciLex
Coordinateur : Chantal Keller
Objectif : Utiliser les preuves comme protocoles de communication entre systèmes de preuves
Financement Labex : 2017

Présentation :
De nombreux paradigmes et systèmes de preuves ont été mis en place pour mécaniser le raisonnement logique: les assistants à la preuve, les démonstrateurs automatiques, les vérificateurs de preuves, les langages de programmation offrant certaines propriétés, le model checking, ... Ce vaste panel permet de satisfaire des objectifs très variés, allant de la démonstration de théorèmes mathématiques abstraits à la certification de logiciels et de matériels.

Si cette multiplicité permet aujourd'hui de vérifier formellement et de manière la plus automatisée possible des énoncés complexes et variés, elle s'accompagne d'une duplication des efforts extrêmement prononcée : en effet, ces systèmes reposent sur des langages de preuves très différents les uns des autres et pouvant difficilement communiquer.

Nous avons pour objectif commun d'explorer les preuves comme protocoles de communication entre systèmes de preuves.

Un premier aspect consiste donc à définir un format de preuve universel pour ce protocole, englobant le plus possible ces systèmes extrêmement différents. Ce format doit permettre non seulement de représenter les preuves mais également de les combiner pour bénéficier des avantages de différents systèmes au sein d'une même preuve. Il pourra reposer sur des frameworks logiques génériques permettant de représenter diverses logiques.

Un deuxième aspect porte sur l'implantation de ce format, à travers des outils de communication entre systèmes et des vérificateurs de preuve universels. Ce travail nécessite d'implanter des encodages entre logiques, des algorithmes pour mettre en relations des énoncés de théorèmes, et des outils efficaces de vérification de preuves.

Enfin, un troisième aspect porte sur la définition et l'implantation de bibliothèques universelles de théorèmes et de preuves. Parmi les sujets possibles, nous proposons de travailler notamment sur des bibliothèques de cryptographie, de théorie des graphes et de résolution de contraintes, avec la volonté de permettre une combinaison d'outils automatiques et interactifs dans l'utilisation de ces bibliothèques.

GT Upscale