Responsables : Évelyne Contejean et Ralf Treinen

• Ralf Treinen (4 cours = 12h)
• Mohamed Iguernelala (4 cours = 12 heures)

• Projet SMT (Mohamed Iguernelala) à rendre pour le 19/03/2015
• Examen final (Ralf Treinen) le 12/03/2015, de 9h45 à 11h45. Tous les documents papier sont autorisés.

Note = (P + E)/2

Le but de ce cours est de fournir aux étudiants les bases nécessaires afin de pouvoir comprendre le fonctionnement de la plupart des outils de démonstration automatique développés en particulier dans le monde académique (voir la page TPTP), et éventuellement de coder eux-mêmes de tels outils.

Naturellement, ce cours est nécessaire pour les étudiants qui poursuivraient ensuite des travaux de recherche dans le domaine de la vérification, de la démonstration automatique ou de la récriture, mais aussi dans des domaines connexes comme la sécurité des systèmes informatiques, les systèmes embarqués, les preuves assistées et plus généralement l'utilisation des systèmes formels.

Dans cette partie du cours nous nous intéressons à des contraintes, c'est-à-dire à des formules de la logique du premier ordre interprétées dans une structure fixée. Une formule avec n variables, interprétée dans une structure fixe, dénote un ensemble de n-uplets de valeurs qui est simplement son ensemble de solutions. La possibilité de combiner des formules par des opérateurs booléens ou des quantificateurs, ensemble avec un algorithme pour décider la satisfaisabilité des formules, nous donne un moyen effectif pour calculer avec des ensembles de n-uplets de valeurs. Des tels mécanismes sont à la base des formalismes computationnels qui manipulent des ensembles de n-uplets de valeurs, comme par exemple la programmation (logique) par contraintes, la réécriture contrainte, ou la vérification de systèmes infinis.
La présentation est organisée autour des méthodes générales. Les méthodes présentées sont illustrées par des systèmes de contraintes utilisées dans les mécanismes mentionnées, typiquement sur des nombres naturels ou des valeurs symboliques (arbres).

• Contraintes de base: simplification, satisfaisabilité, implication
• Élimination de quantificateurs
• Méthodes basées sur des classes d'automates
• Méthodes pour les preuves de non-décidabilité de théories

• SAT solveurs modernes (back-jumping, learning), MiniSat ;
• interaction entre SAT et une procédure de décision pour une théorie T : DPLL(T) ;
• exemples de théories qui ont une procédure de décision :
  • tableaux ;
  • arithmétique linéaire ;
  • égalité
• combinaison de procédures de décision ;
• traitement des quantificateurs par le mécanisme des déclancheurs (triggers) ;
• exemples de solveurs SMT : Alt-Ergo, CVS4, Simplify, Yices, Z3

• 11 décembre Ralf Treinen
• 18 décembre Ralf Treinen
• 8 janvier Ralf Treinen
• 15 janvier Ralf Treinen
• 22 janvier Mohamed Iguernelala
• 29 janvier Mohamed Iguernelala
• 5 février Mohamed Iguernelala
• 12 février Mohamed Iguernelala
• 12 mars : examen final (voir les modalités d'évaluation plus haut)

Notions de logique du premier ordre, savoir ce qu'est une règle d'inférence.

• Français par défaut / French by default

• Les langues autorisées pour l'examen sont le français et l'anglais.

Le polycopié et les transparents de la partie de Ralf Treinen se trouvent sur http://www.pps.univ-paris-diderot.fr/~treinen/teaching/mpri2.5/.
Le polycopié contient plus de matériel que ce que l'on peut effectivement traiter en 4 session de cours.

• Recommandé :
  • 2-36-1 preuve de programmes
  • 2-7-1 fondements des systèmes de preuves
  • 2-7-2 : assistants de preuves

• Pour la culture

L'essentiel du cours se trouve dans

• A. Robinson and A. Voronkov eds, Handbook of Automated Reasoning, vols 1 & 2, North Holland, 2001.
• Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite systems, Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics, MIT Press, Cambridge, MA, 1991

Sur des parties importantes du cours:

• Jean Goubault-Larrecq and Ian Mackie, Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer Academic, 1997.
• Franz Baader and Tobias Nipkow, Term Rewriting and all that, Cambridge University Press, 1998.
• Ralf Treinen, Constraint Solving and Decision Problems of First-Order Theories of Concrete Domains, notes de cours, 2010.