Outils
Logiques
Liens
Page du cours de Roberto
Amadio
Installation de SATO
Pour me contacter : delatail@pps.jussieu.fr
Énoncés de TD
Feuilles de TD
Interro du 22/11/2006 et correction
Énoncés de TP
TP1 : implémentation de
l'algorithme de Davis-Putnam
Une correction (simple mais succinte) pour
la lecture / écriture dans un fichier (fichier d'exmple : entree.cnf)
TP2 : utilisation de SATO pour un
problème d'emploi du temps
TP3 :
version 1 :
implémentation de l'algorithme
de résolution unitaire
version 2
(conseillée) : algorithme de résolution, étape par
étape