Thursday 27 October 2016, 14:00, LSV: Reconstruction de preuves au format TSTP pour Dedukti (short talk), David Pham (ENSIIE intern).

La démonstration permet d'établir un énoncé mathématique à partir de propositions initiales, en s'appuyant sur un ensemble de règles de déduction. La preuve automatique de théorème consiste à laisser l'ordinateur prouver les propriétés automatiquement, étant donnés une description du système, un ensemble d'axiomes et un ensemble de règles d'inférences.
L’équipe Deducteam du LSV développe un format de preuves qui se veut universel. Le but est de pouvoir être capable de vérifier des preuves provenant de différents systèmes de preuve, voire de pouvoir les combiner.
Zenon Modulo, un système de preuve automatique, est capable de produire des preuves dans un format sûr appelé Dedukti. Néanmoins Zenon Modulo est moins efficace que d’autres comme par exemple Eprover.
L’idée est donc de s’aider des traces de preuves produites par les autres prouveurs pour guider Zenon Modulo, dans sa recherche de preuve. Pour cela, nous utilisons deux techniques de preuve qui sont la sélection d’axiome et la reconstruction de preuves.
L'objectif de ce stage est de transformer des traces de preuves au format TSTP, obtenues grâce au prouveur E sur la bibliothèque de fichiers problèmes TPTP, en preuves formelles pour le vérificateur de preuves universel Dedukti. Pour cela, il faut étendre Zenon Modulo de façon ça : reconstruire les preuves Dedukti en n'utilisant que les axiomes réellement nécessaires à la preuve et reconstruire les preuves Dedukti en reprouvant chaque étape de la trace de preuve et en les combinant.