Description
Date depot: 1 janvier 1900
Titre: Déduction automatique modulo
Encadrant :
Damien DOLIGEZ (Inria-Paris (ED-130))
Directeur de thèse:
David DELAHAYE (LIRMM)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
{{Encadrants:}}
Cette thèse sera co-encadrée par David Delahaye (CNAM), Damien Doligez (INRIA), et Olivier Hermant (ISEP).
{{Sujet:}}
En déduction automatique (domaine qui a pour objectif de prouver automatiquement des théorèmes), la tendance actuelle consiste à développer des fondements théoriques, ainsi que des outils pratiques, qui visent à démontrer efficacement des théorèmes qui utilisent des théories. Dans ce domaine, certaines méthodes de déduction modernes tendent à donner des résultats très prometteurs. En particulier, c'est le cas de la déduction modulo [5], qui présente la théorie sous la forme d'un système de réécriture au lieu d'axiomes, transformant des étapes de déduction en calculs et permettant ainsi de produire des preuves plus courtes.
L'objectif de cette thèse est d'intégrer la déduction modulo à un outil de démonstration automatique au premier ordre, en particulier l'outil Zenon. Le prouveur Zenon [2] est un outil basé sur la méthode des tableaux avec égalité, et qui a pour caractéristique d'être à la fois extensible (possibilité de rajouter des règles de déduction spécifiques) et certifiant (les preuves produites peuvent être vérifiées par d'autres outils d'aide à la preuve comme Coq ou Isabelle). Pour réaliser cette intégration, on pourra s'inspirer d'une expérimentation récente [6], qui a consisté à étendre Zenon à la superdéduction [4], à savoir une variante de la déduction modulo où la théorie est présentée sous la forme de sur-règles de déduction (règles de déduction compilées).
L'intégration de la déduction modulo à Zenon visera également à développer un nouveau « backend » pour Zenon (autre que ceux vers Coq et Isabelle), en utilisant le « logical framework » Dedukti. L'outil Dedukti [8] est un vérificateur de preuve universel, basé en particulier sur le λΠ-calcul modulo (λ-calcul avec types dépendants en déduction modulo), ce qui en fait un candidat idéal pour encoder les preuves modulo théories. Un autre intérêt de Dedukti réside dans l'interopérabilité des preuves, en ce sens que les preuves Dedukti peuvent être réutilisées dans le cadre de plusieurs théories.
Afin de tester l'intégration de la déduction modulo à Zenon, un autre objectif de cette thèse est de réaliser une instanciation avec la théorie des ensembles de la méthode B [1] (méthode permettant la conception de logiciels sûrs). Cette instanciation devrait permettre de vérifier automatiquement des obligations de preuve provenant de la formalisation d'applications B, ainsi que des règles de preuve de l'Atelier B, qui est un outil industriel implantant la méthode B. Cette expérimentation se situe dans la lignée des travaux réalisés en collaboration avec l'entreprise Siemens [7], où Zenon a pu être utilisé dans la vérification de règles B provenant d'une base de règles maintenue par Siemens.
Enfin, cette thèse comporte également un pan plus théorique avec notamment une étude fondamentale de l'extension de Zenon à la déduction modulo, ainsi que l'instanciation à la théorie des ensembles de B, toutes deux précédemment réalisées. Plusieurs propriétés devront être établies formellement, comme la cohérence et la complétude [3] (relatives ou non) de ces méthodes, notamment la complétude de l'algorithme de recherche de preuve de Zenon, qui devra également être établie, en présence de déduction modulo ou non (cette propriété n'ayant pas encore été établie pour Zenon sans déduction modulo).
{{Références:}}
-# J.-R. Abrial. {The B-Book, Assigning Programs to Meanings.} Cambridge University Press, Cambridge (UK), 1996. ISBN 0521496195.
-# R. Bonichon, D. Delahaye, and D. Doligez. Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In {Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, volume 4790 of {LNCS/LNAI}, pages 151–165, Yerevan (Armenia), Oct. 2007. Springer.
-# R. Bonichon and O. Hermant. A Semantic Completeness Proof for TaMeD. In {Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, volume 4246 of {LNCS}, pages 167-181, (Phnom Penh) Cambodia, Nov. 2006. Springer.
-# P. Brauner, C. Houtmann, and C. Kirchner. Principles of Superdeduction. In {Logic in Computer Science (LICS)}, pages 41–50, Wrocław (Poland), July 2007. IEEE Computer Society Press.
-# G. Dowek, T. Hardin, and C. Kirchner. Theorem Proving Modulo. {Journal of Automated Reasoning (JAR)}, 31(1):33–72, Sept. 2003.
-# M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois. Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. In {International Joint Conference on Automated Reasoning (IJCAR)}, Manchester (UK), June 2012. Springer. To appear.
-# M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois. Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving. In {Software Engineering and Formal Methods (SEFM)}, volume 7041 of {LNCS}, pages 253–268, Montevideo (Uruguay), Nov. 2011. Spr
Doctorant.e: Halmagrand Pierre