Résolution de contraintes

(Partie du cours 2-5 Démonstration Automatique)

MPRI, 2ème année, 2010/2011
Mardi, 16h15 à 18h45, salle Chevaleret 0D4.

Notes de cours

Le poly complet (format postscript gzippé) dans la version 2.2 du 31 janvier 2011. Le poly contient évidemment beaucoup plus de matériel que ce qu'on peut effectivement couvrir en 12 heures de cours. Je vais distribuer des copies du poly au premier cours.

Planning (préliminaire)

Mardi 1/2 Introduction, résolution de contraintes basiques par simplification
Mardi 8/2 Élimination de quantificateurs
Mardi 15/2 Résolution de contraintes par saturation.
Mardi 22/2 Techniques basées sur les automates
Mardi 1/3 Systèmes de contraintes non-décidables

Stage de Recherche

Ralf Treinen