– ASAP

Le but de ce projet est de développer des formalismes logiques permettant de représenter et manipuler des schémas de formules et de preuves en déduction interactive (ou automatique) et d'utiliser ces outils pour aider à la formalisation et à l'analyse de preuves mathématiques (en utilisant des techniques de transformation de preuves par élimination de coupures). Les schémas que nous considérons sont des schémas d'itération qui sont souvent utilisés en mathématiques et en informatique (des exemples typiques sont le principe du pigeonnier ou le théorème de Ramsey). Ces schémas apparaissent également fréquemment en vérification de circuit ou de programme où les formules spécifiant le problème à résoudre sont souvent paramétrées par un entier naturel dénotant par exemple le nombre de bits, la taille des données etc. Raisonner sur de tels schémas de formule est difficile et requiert en général l'utilisation d'une forme spécifique d'induction mathématique. Concevoir des procédures de preuve capable de traiter ces schémas de manière automatique augmenterait significativement le pouvoir d'expression des langages existants et permettrait d'obtenir des preuves plus courtes, plus éclairantes et plus structurées. L'utilisation de schémas de formules est extrêmement utile pour la formalisation des preuves mathématiques parce qu'elle permet d'exprimer de manière naturelle et efficace des séquences infinies de pas d'inférence. Cette idée a été mise en oeuvre dans le système HLK/CERES (développé par le partenaire n°2) pour l'analyse des preuves mathématiques afin de formaliser des preuves par induction en évitant d'avoir à utiliser un langage plus expressif (pour lequel aucune procédure de preuve adéquate n'existe). Cependant, la version actuelle du système permet seulement de définir de telles séquences itérées. Les schémas obtenus doivent être ensuite transformés en des preuves standards par instantiation avant de pouvoir être traités. Notre objectif dans ce projet est de développer des outils pour traiter et pour prouver ces séquences directement au niveau objet (de manière automatique ou interactive). Plus précisément, nous cherchons à définir des formalismes logiques intermédiaires, dont le pouvoir d'expression serait plus grand que le langage de base (en général la logique d'ordre 1) mais inférieur à celui des langages d'ordre supérieur. Le langage obtenu devra être plus expressif par certains aspects que le langage originel et autoriser une formalisation plus naturelle et plus concise des preuves mais il devra aussi préserver (lorsque cela est possible) les bonnes propriétés computationnelles du langage de base, par exemple la décidabilité ou la complétude. Les améliorations qualitatives qu'apporterait la réussite de ce projet aux démonstrateurs automatiques et assistants de preuve ont été identifiées depuis longtemps comme très souhaitables par les utilisateurs de ces systèmes, en particulier par les mathématiciens. Ce projet, centré sur la schematisation de formules et de preuves et sur leurs applications en formalisation des mathématiques, est directement relié à l'axe thématique "Mathématiques" de l'AAP ainsi qu'à la logique, la théorie de la preuve et évidemment la déduction automatique. Il n'existe à notre connaissance aucun projet poursuivant des buts similaires.