[LO5] Logique 2021–2022

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

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 13/09.

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 13/09
⚠️ amphi en salle 2A
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
fichier Formule.java
⚠️ pas de TD
semaine du 20/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.3. Substitutions propositionnelles
semaine du 27/09
TD n°2
4.4. Équivalences usuelles
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 04/10
⚠️ QCM₁ à 10:45 le 06/10 en amphi 1A
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)
semaine du 11/10
TD n°4
MP1 à rendre pour le 29 octobre
exemples de fichiers DIMACS
exemple d'implémentation Java
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 18/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 25/10
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 29 octobre
semaine du 01/11
vacances
semaine du 08/11
⚠️ amphi en salle 2A
12.2. Modèles, satisfiabilité et validité
13. Substitutions
13.2. α-renommages
semaine du 15/11
14.1. Forme normale négative
14.2. Forme prénexe
14.3. Skolémisation
semaine du 22/11
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 29/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 ; 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 06/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 13/12
⚠️ pas de cours magistral

Autres ressources pédagogiques

Ouvrages

Notes de cours

Années précédentes