Projet réécriture (Évelyne Contejean et Xavier Urbain)
Examen final (Évelyne Contejean, Xavier Urbain et Ralf Treinen)
Note = max (E, (DM + P + 2E)/4)
Objectifs
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.
Plan du cours pour 2009-2010
Jean Goubault-Larrecq (4 cours): Techniques de résolution.
logique du premier ordre, sémantique de Tarski.
formes clausales, indécidabilité.
théorème de compacité de la logique du premier ordre,
théorème de Herbrand, arbres sémantiques.
la règle de résolution, complétude par arbres sémantiques,
premier raffinement: la résolution ordonnée.
complétude en présence de règles de simplification
(tautologies, clauses subsumées), et jeux sur arbres
sémantiques.
deuxième raffinement: résolution ordonnée avec fonction
de sélection.
application à la décidabilité de certaines classes de
la logique du premier ordre, principalement la classe
monadique.
relation avec automates d'arbres, contraintes ensemblistes,
la classe décidable H1, application à la vérification
de protocoles cryptographiques. L'outil h1.
Note
l'application à la vérification de protocoles
cryptographiques sera relativement sommaire, mais
complémentaire du cours de sécurité de B. Blanchet,
D. Pointcheval, S. Kremer.
Évelyne Contejean (2 cours) : Logique équationnelle et récriture
logique équationelle, problème du mot, problème d'unification.
récriture standard, modulo (cas général et AC)
matching et unification modulo, combinaison d'algorithmes d'unification.
Xavier Urbain (4 cours) : Techniques de terminaison
terminaison : généralités, critères, modularité
ordres bien-fondés
terminaison modulo
stratégies
certificats de terminaison
Évelyne Contejean (2 cours) : Completion et clôture de congruence.
confluence locale, lemme des paires critiques
convergence, décision du problème du mot
complétion, récriture de preuves, critères d'élimination des paires critiques
Ralf 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.
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
Pré-requis
Notions de logique du premier ordre, savoir ce qu'est une règle d'inférence.
Langues du cours :
Jean Goubault-Larrecq fera son cours en anglais si au moins un
étudiant le demande, et sinon en français.
Évelyne Contejean et Xavier Urbain feront leur cours en français, mais répondront aux
questions des étudiants en anglais si ceux-ci le demandent.
Ralf Treinen fera son cours en anglais si au moins un
étudiant le demande, et sinon en français. Le polycopié utilisé
pour cette partie du cours est en anglais.
Les langues autorisées pour l'examen sont le français et l'anglais.
Supports de cours :
Jean Goubault-Larrecq fournit un polycopié en français sur le Web,
et un article en anglais recouvrant en gros les memes thèmes
pour les anglophones.
Évelyne Contejean et Xavier Urbain fournissent un polycopié en français version 2007. Celui-ci sera
traduit en anglais si des étudiants le demandent.
Ralf Treinen va distribuer un polycopié en anglais à sa première session de cours. Vous
pouvez consulter une version ancienne.
Le polycopié sera revisé pour cette année, il contient plus de matériel qu'on peut effectivement traiter
en 4 session de cours.
Cours liés :
Recommandé :
Pour la culture
Bibliographie
L'essentiel du cours (en dehors des applications à la sécurité)
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.
