Le groupe Lemme s'intéresse au développement de programmes de calcul symbolique certifiés et efficaces. Pour cela on utilise l'assistant de preuve Coq pour développer en parallèle l'algorithme et sa preuve de correction. Les algorithmes définis dans Coq peuvent ensuite être efficacement compilés en OCaml.
Dans ce stage on s'intéressera aux formules booléennes. Une formule booléenne est formée d'un ensemble de connecteurs logiques (ou, et, implique, etc) et d'un ensemble de variables. Une formule booléenne est satisfiable, si il existe des valeurs de ses variables qui la rende vraie. Ce problème a été un des premiers à avoir être prouvé NP-complet. Cependant trouver un algorithme efficace qui détermine si une formule donnée est satisfiable reste un sujet de recherche des plus actifs. Les logiciels pour prouver la satisfiabilité devenant de plus en plus complexes, assurer leur correction est problématique. Le but de ce stage est de montrer qu'il est possible de développer un programme certifié qui teste la satisfiabilité de formules booléennes. Pour définir ce programme on s'inspirera des algorithmes présents dans le programme Heerhugo développé à Eindhoven.
E-mail : Laurent.Thery@sophia.inria.fr
[1] J.F. Groote and J.P. Warners. The propositional formula checker HeerHugo. Journal of Automated Reasoning, 24:101-125, 2000.
[2] G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA 0204, août 1997.
[3] Pierre Letouzey, Stalmarck's algorithm in Coq, TPHOLs2000, LNCS 1869 pp 387-404.Janvier 2001.