Démonstration automatique
Présentation
Historiquement, la démonstration automatique est divisée en deux
courants principaux, celui qui est basé sur les techniques de
résolution, de récriture et d'unification, et celui basé sur la
combinaison de procédures de décision. Depuis une vingtaine
d'années, notre équipe travaille sur la récriture et a développé la
boîte à outils
CiME, puis sa bibliothèque de certification en Coq
Coccinelle. Plus récemment, nous nous sommes intéressés à la
seconde approche, en développant le démonstrateur
Alt-Ergo. Un de
nos objectifs actuels est d'intégrer des techniques de récriture au
coeur même d'
Alt-Ergo, afin d'augmenter sa puissance et son
expressivité.
Thématiques
Récriture
La récriture de termes est une technique pour traiter l'égalité
en démonstration automatique : alors qu'une équation peut être
utilisée dans les deux sens, une règle de récriture ne peut
s'appliquer que de gauche à droite. Par exemple, le système ci-dessous
modélise les groupes non commutatifs suivant la définition
mathématique usuelle :
| (x . y) . z | = | x . (y . z) | (A) |
| x . e | = | x | (N) |
| x . i(x) | = | e | (I) |
|
Avec ces égalités, il est possible de montrer que
i(
e) =
e grâce aux étapes suivantes :
| i(e) | =N | i(e) . e |
| | =I | i(e) . (i(e) . i(i(e))) |
| | =N | i(e) . (i(e) . i(i(e).e)) |
| | =I | i(e) . (i(e) . i(i(e).(e.i(e)))) |
| | =A | i(e) . (i(e) . i((i(e).e).i(e))) |
| | =N | i(e). (i(e) . i( i(e).i(e) )) |
| | =A | (i(e). i(e)) . i( i(e).i(e) )) |
| | =I | e |
|
La transformation de l'ensemble d'égalités en système de
récriture soulève plusieurs problèmes.
| (x . y) . z | → | x . (y . z) | (A) |
| x . e | → | x | (N) |
| x . i(x) | → | e | (I) |
|
Tout d'abord, il n'est plus possible de montrer que
i(
e)
=
e, puisqu'aucun des deux termes de l'égalité ne se réduit. La
deuxième question de garantir qu'un terme ne pourra pas réduire
indéfiniment, sans atteindre un résultat en un temps fini. Les propriétés
correspondantes sont connues sous les noms de confluence et terminaison.
La complétion est une manière de restaurer la confluence, mais le processus
peut ne pas terminer, et donne seulement une procédure de semi-décision.
Depuis une dizaine d'années, la recherche sur la terminaison est un domaine
très actif en démonstration automatique : de nombreux critères de terminaison
ont été proposés et implantés dans plusieurs outils. Depuis 2003, il y a une
compétition de terminaison, qui a mis en évidence que tous les outils
participants ont au moins une fois utilisé un argument non valable dans
leurs démonstrations.
Nous travaillons sur les moyens de certifier certains des algorithmes à
l'oeuvre dans les outils pour la récriture, et également certaines propriétés
des systèmes de récriture, comme l'égalité modulo et la terminaison. Pour celà,
nous développons
Coccinelle, la bibliothèque Coq compagne de
CiME notre boîte
à outils pour la récriture.
Coccinelle contient une modélisation en Coq des
notions suivantes :
- termes et récriture ;
- certains des algorithmes cruciaux de CiME, tels que :
- unification ;
- filtrage modulo les symboles associatifs et commutatifs ;
- ordre RPO ;
- des critères de termiaison puissants ;
Coccinelle peut donc être utilisée pour vérifier qu'un certificat de terminaison est
valide, c'est-à-dire que lorsqu'un théorème est appliqué, toutes ses prémisses sont
satisfaites.
Combinaison de procédures de décision
Le démonstrateur automatique
Alt-Ergo appartient à la famille
des démonstrateurs SMT (Satisfiability Modulo Theory). Il est
spécialement conçu pour prouver la validité de formules issues de la
preuve de programme. La syntaxe d'entrée d'
Alt-Ergo est une logique
du premier ordre étendue avec des théories prédéfinies et des types
polymorphes. Les théories prédéfinies dans
Alt-Ergo sont les
suivantes:
- égalité avec symboles non-interprétés;
- arithmétique sur les entiers et les rationnels;
- tableaux polymorphes;
- vecteurs de bits de taille fixes;
- types énumérés;
- symboles associatifs-commutatifs définis par l'utilisateur.
Personnes
François Bobot,
Sylvain Conchon,
Évelyne Contejean,
Claire Dross,
Mohamed Iguernelala,
Alain Mebsout,
Andrei Paskevich,
Xavier Urbain
Outils
- Alt-Ergo, un solveur SMT dédié à la preuve de programme
- CiME, une boîte à outils pour la récriture
- Coccinelle, sa bibliotèque Coq associée
Contrats
Publications principales
- [1]
- Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala.
Canonized Rewriting and Ground AC Completion Modulo Shostak
Theories. In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Saarbrücken, Germany, April 2011. Springer.
[ bib ]
- [2]
- Stéphane Lescuyer and Sylvain Conchon.
Improving Coq propositional reasoning using a lazy CNF conversion
scheme. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of
Combining Systems, 7th International Symposium, Proceedings, volume 5749 of Lecture Notes in Computer Science, pages 287-303, Trento, Italy,
September 2009. Springer.
[ bib |
DOI ]
- [3]
- François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane
Lescuyer.
Implementing Polymorphism in SMT solvers.
In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th
International Workshop on Satisfiability Modulo, volume 367 of ACM
International Conference Proceedings Series, pages 1-5, 2008.
[ bib |
PDF |
.pdf ]
- [4]
- Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
theories.
In Proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198-2 of Electronic
Notes in Computer Science, pages 51-69. Elsevier Science Publishers, 2008.
[ bib ]
- [5]
-
Stéphane Lescuyer and Sylvain Conchon.
A reflexive formalization of a SAT solver in Coq.
In Emerging Trends of the 21st International Conference on
Theorem Proving in Higher Order Logics, 2008.
[ bib ]