L'organisation de cet enseignement est modifiée en raison de la
pandémie. Les cours magistraux n'auront pas lieu en
présentiel. Des vidéos sont mises en ligne chaque semaine pour
compléter la lecture des notes de cours,
avec des séances de questions/réponses
organisées en distanciel.
Les séances de travaux dirigés auront également lieu en distanciel.
Modalités de contrôle des connaissances
Tout se passe sur
la page
Moodle du cours.
- QCM1, QCM2
: deux questionnaires à choix multiples, chacun 10% de la
note finale
- MP1, MP2
: deux mini-projets à réaliser en binômes (mêmes binômes pour
les deux rendus), chacun 15% de la
note finale
- DM1, DM2
: deux devoirs maison, chacun 25% de la note finale
Matériel pédagogique
Voir
la page
Moodle du cours pour les rendus de QCM, projets et devoirs
maison notés.
Les notes de cours ont été mises à jour
le 12/12.
Programme
Les numéros comme 1. Contexte et motivations
ou 2. Syntaxe
font références aux numéros des sections
correspondantes dans les notes de
cours. Les
icônes , et indiquent du matériel disponible
sous forme de vidéos sur youtube, de discussions sous discord, ou
depuis la page Moodle. Les sections « grisées » et
marquées d'une étoile sont facultatives : il n'y aura
pas de questions qui portent dessus lors des TDs, QCMs, DMs,
etc.
Première partie : logique propositionnelle
Les exemples d'implémentation issues des notes de cours sont
disponibles : Java, DIMACS.
- semaine du 07/09
- 0. Organisation du
cours
1. Contexte et motivations
2.1. Arbres de syntaxe abstraite
2.2. Syntaxe concrète
3.1.1. & 3.1.2. Interprétations et
sémantique
2.1.1. & 3.1.3.
Syntaxe et sémantique en Java sur #qa-09-09-2020
;
fichier Formule.java
à compléter
⚠️ pas de TD
- semaine du 14/09
-
TD n°1 ;
corrigé exo
1,
exo 2
exercice d'implémentation
de la méthode Formule.toString()
corrigé sur #qa-16-09-2020
3.1.3. Sémantique en Java sur #qa-16-09-2020
3.1.5. Tables de vérité
3.1.6. Étendre la syntaxe
3.1.7. Complétude fonctionnelle
3.2. Satisfiabilité et validité
4.1. Conséquences logiques
4.2. Équivalences logiques
4.3. Substitutions
propositionnelles
4.3.1. Substitutions propositionnelles
en Java sur #qa-16-09-2020
4.4. Équivalences usuelles
- semaine du 21/09
-
TD n°2 ;
corrigé exo
2,
exo 3,
exo 5,
exo 6
5.1. Forme normale négative
5.1.1. Formes normales négatives en
Java sur #qa-23-09-2020
5.2.1. & 5.2.3. Forme clausale
équivalente et format DIMACS
5.2.2. Forme clausale équi-satisfiable
5.2.4. Implémentation de la forme clausale en Java
5.3. Forme normale disjonctive
- semaine du 28/09
-
TD n°3 ;
exo 1
(intro), exo 1
(correction), exo 2a
(intro), exo
2a
(correction), exo
2b, exo
3a
QCM1
le 30 septembre à 13:30 sur la page Moodle
exercice d'implémentation
de la méthode Formule.getCNF()
corrigé sur #qa-30-09-2020
6.1. Utilisation de solveurs SAT
(fichier DIMACS
)
6.2. Exemple de modélisation : coloration de
graphe (fichier DIMACS
)
6.3. Exemple de modélisation : dépendances
logicielles
(fichier DIMACS
)
- semaine du 05/10
-
TD n°4 ; exo 1 (a–c), exo 1 (d–f), exo 2 (intro), exo 2 (a), exo 2
(b), exo 3
(d–e)
MP1 à rendre pour le 28
octobre
code
OCaml pour la logique propositionnelle sur #qa-07-10-2020
7.1. Recherche de modèle par
énumération
7.1.1. Implémentation de la recherche par
énumération en Java
7.2. Recherche de modèle par
simplification
7.2.3. Correction et complétude de la
recherche par simplification
7.2.4. Implémentation de la recherche par
simplification en Java
7.3. Algorithme
de Davis, Putnam, Logemann
et Loveland
7.3.1. & 7.3.2. Correction de l'algorithme
DPLL
7.3.3. Implémentation d'un DPLL récursif en Java
7. bonus : Comparaisons des performance des solveurs SAT
- semaine du 12/10
-
TD n°5 ; correction
exo 1 (a),
exo 1
(b–c), exo 1 (d–e),
exo 3
8. Validité et certificats
8.1. Calcul des séquents propositionnel
8.2. Recherche de preuve
8.2.1. Inversibilité et algorithme de recherche de preuve
8.2.2. Implémentation de la recherche de
preuve en Java
8.3. Théorème 8.10 de correction
8.3. Théorème 8.13 de complétude
- semaine du 19/10
-
TD n°6 ; correction
exo 2
9. * Clauses de Horn
9.1. * Modèle minimal
9.2. *
HornSAT
9.2.3. *
Algorithme
pour HornSAT en
temps linéaire
9.2.5. *
Implémentation de l'algorithme en temps linéaire en OCaml sur #qa-21-10-2020
9.3. * Exemple de modélisation : accessibilité dans un
graphe orienté
- semaine du 26/10
- ⚠️ rappel : MP1 à rendre pour le 28
octobre
DM1 à rendre pour le 12 novembre
Deuxième partie : logique du premier ordre
- semaine du 02/11
-
TD n°7 de révision sur la
logique propositionnelle ;
correction exo 3
Petit retour sur la modélisation sur
#qa-04-11-2020
Introduction de la partie 3 sur la logique
classique du premier ordre
10–12. Introduction à la syntaxe et à la
sémantique de la logique du premier ordre
- semaine du 09/11
- TD n°8 ; correction
exo 3(a)1
⚠️ rappel : DM1 à rendre pour le 12
novembre
séance de questions/réponses asynchrone
sur #qa-11-11-2020
pour cause de jour férié
10. Structures
11. Syntaxe de la logique du premier
ordre
12.1. Sémantique de la logique du premier
ordre
12.2. Modèles, satisfiabilité et validité
- semaine du 16/11
-
TD n°9 ; correction
exo 2
13. Substitutions
13.2. α-renommages
14.1. Forme normale négative
14.2. Forme prénexe
14.3. Skolémisation
- semaine du 23/11
-
TD n°10
15. Théories logiques
15.1.1. Théories de structures
15.1.2. Théories axiomatiques
15.1.3. Interprétations normales
15.1.4. Cohérence, complétude et décidabilité
15.2. Élimination des quantificateurs
15.2.2. Théorie des ordres denses linéaires non bornés
15.2.3. Théorie de l'arithmétique linéaire rationnelle
- semaine du 30/11
-
TD n°11
QCM2
le 30 novembre à 16:15 sur la page Moodle
MP2 à rendre pour le 16 décembre
16. Satisfiabilité modulo théorie
16.1.1. Principes de base des solveurs SMT
16.1.2. Élimination des quantificateurs
16.1.3. SMT-LIB sous forme de page web
interactive ; voir aussi
le tutoriel Z3 et les exemples
de fichiers au format SMT-LIB
16.1.4. Théories usuelles, tiré de la
documentation de SMT-LIB
16.2. Exemple de modélisation : nombre de
McNuggets ; fichier SMT-LIB
16.3. Exemple de modélisation :
apprentissage d'automate
séparateur ; énoncé
du problème ; formalisation ; modélisation
comme un problème de satisfiabilité modulo théorie ;
modélisation en
SMT-LIB ; fichier SMT-LIB
16.4. Exemple de modélisation : synthèse
d'invariant de
programme ; fichier SMT-LIB
- semaine du 07/12
-
TD n°12
17. Calcul des séquents du premier ordre ;
Exemple 17.4
17.1. Correction du calcul des séquents du
premier ordre
17.2. * Règles admissibles du calcul des séquents
17.3. * Complétude du calcul des séquents
17.4. * Élimination des coupures en calcul des séquents
- semaine du 14/12
- ⚠️ rappel
: MP2 à rendre pour le 16
décembre
DM2 à rendre pour le 11 janvier
- semaine du 11/01
- ⚠️ rappel : DM2 à rendre pour le 11
janvier