[LO5] Logique 2020–2021

3e année de licence d'informatique, UFR informatique, Université de Paris

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.

Séances et intervenants

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

Autres ressources pédagogiques

Ouvrages

Notes de cours

Années précédentes