Table of Contents
Démonstration automatique (24h, 3 ECTS)Responsables : Évelyne Contejean et Ralf Treinen Intervenants prévus pour 2014-2015
Évaluation
Note = (P + E)/2 ObjectifsLe 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. Plan du cours pour 2014-2015Ralf Treinen (4 cours) : Résolution de contraintes symboliques et théories du premier ordre
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.
Mohamed Iguernelala (4 cours) : Solveurs Modulo Théories (SMT)
Planning:
Pré-requisNotions de logique du premier ordre, savoir ce qu'est une règle d'inférence. Langues du cours :
Supports de cours :
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/. Cours liés :
BibliographieL'essentiel du cours se trouve dans
Sur des parties importantes du cours:
Équipe pédagogique
|