[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 23/10.

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.

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/09 à 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)
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
La section 9 du cours est facultative : il n'y aura pas de questions qui portent dessus lors des TDs, QCMs, DMs, etc.
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
semaine du 26/10
rappel : MP1 à rendre pour le 28 octobre
semaine du 02/11
TD n°7

Autres ressources pédagogiques

Ouvrages

Notes de cours

Années précédentes