[LO5] Logique 2022–2023

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

Modalités de contrôle des connaissances

Tout se passe sur la page Moodle du cours.

Séances et intervenant·e·s

Matériel pédagogique

notes de cours ; dernière mise à jour le 05/09
page Moodle du cours

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 indiquent des vidéos sur youtube sur le contenu du cours.

Première partie : logique propositionnelle

semaine du 12/09
⚠️ pas de TD
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
3.1.5. Tables de vérité
fichier Formule.java
semaine du 19/09
TD n°1
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.4. Équivalences usuelles
semaine du 26/09
⚠️ QCM₁ pendant les TD
TD n°2
4.3. Substitutions propositionnelles
5.1. Forme normale négative
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 03/10
TD n°3
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)
7.1. Recherche de modèle par énumération
7.1.1. Implémentation de la recherche par énumération en Java
semaine du 10/10
TD n°4
MP1 à rendre pour le 28 octobre ; exemples de fichiers DIMACS ; exemple d'implémentation 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 17/10
TD n°5
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

Deuxième partie : logique du premier ordre

semaine du 24/10
⚠️ PA pendant les TD ; durée : 1h30, tous documents papiers autorisés, programme : la première partie (sections 1–8, TD 1–5)
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
10. Structures
11. Syntaxe de la logique du premier ordre
12.1. Sémantique de la logique du premier ordre
⚠️ ne pas oublier le MP1 à rendre pour le 28 octobre
semaine du 31/10
vacances
semaine du 07/11
TD n°6
12.2. Modèles, satisfiabilité et validité
13. Substitutions
13.2. α-renommages
semaine du 14/11
TD n°7
⚠️ séance de rattrapage de TD du groupe 2 le 16/11 à 10:45–12:45 en salle 0014
14.1. Forme normale négative
14.2. Forme prénexe
14.3. Skolémisation
15. Théories logiques
15.1.1. Théories de structures
15.1.2. Théories axiomatiques
semaine du 21/11
⚠️ QCM₂ à 11:00 le 22/11 en amphi 8C, programme : sections 10–13 des notes de cours
TD n°08
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 28/11
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 (rise4fun is down 😢) ; 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 05/12
semaine du 12/12
⚠️ pas de cours magistral
semaine du 02/01
⚠️ EX présentiel le 03/01/2023, 13:30–16:30 en salles 6E - 3B - 226C. Tous documents papier autorisés.

Autres ressources pédagogiques

Ouvrages

Notes de cours

Années précédentes