[LO5] Logique 2023–2024

Modalités de contrôle des connaissances

Tout se passe sur la page Moodle du cours.

• QCM₁, QCM₂ : deux questionnaires à choix multiples, chacun 10% de la note finale
• MP₁, MP₂ : deux mini-projets à réaliser en binômes (mêmes binômes pour les deux rendus), chacun 10% de la note finale
• PA: partiel pour 20% de la note finale
• EX : examen, pour 40% de la note finale

Séances et intervenant·e·s

• cours magistraux : lundi 13:45—15:45 amphi 8C (Sylvain Schmitz)
• travaux dirigés groupe 1 : mardi 08:30—10:30 Halle aux farines 279F (Clément Blaudeau)
• travaux dirigés groupe 2 : vendredi 10:45—12:45 Halle aux farines 279F (Mohammed Foughali)
• travaux dirigés groupe 3 : lundi 16:00—18:00 Olympe de Gouge 118 (Mohammed Foughali)
• travaux dirigés groupe 4 : mercredi 08:30—10:30 Sophie Germain 2035 (Jérémie Marquès)
• travaux dirigés groupe 5 : lundi 10:45–12:45 Halle aux farines 471E 29/09, 02/10 et 18/12 sinon Olympe de Gouges 203 (Jérémie Marquès)

Matériel pédagogique

notes de cours ; dernière mise à jour le 04/12
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 18/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é
3.1.6. Étendre la syntaxe

semaine du 25/09

TD n°1
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.4. Équivalences usuelles
5.1. Forme normale négative

semaine du 02/10

TD n°2
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
6.1. Utilisation de solveurs SAT (fichier DIMACS)
6.3. Exemple de modélisation : dépendances logicielles (fichier DIMACS)

semaine du 09/10

⚠️ QCM₁ pendant les TD, programme : sections 1–4 des notes de cours
TD n°3
6.2. Exemple de modélisation : coloration de graphe (fichier DIMACS)
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

semaine du 16/10

MP₁ à rendre pour le 3 novembre ; exemples de fichiers DIMACS
TD n°4
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
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

Deuxième partie : logique du premier ordre

semaine du 23/10

TD n°5
8.3. Théorème 8.13 de complétude
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

semaine du 30/10

🏝️ semaine de pause
⚠️ MP₁ à rendre pour le 03/10

semaine du 06/11

⚠️ PA pendant le CM ; durée : 1h, tous documents papiers autorisés, programme : la première partie (sections 1–8, TD 1–5) ; annale : partiel 2020–2021
TD n°6
12.2. Modèles, satisfiabilité et validité

semaine du 13/11

TD n°7
12.2. Modèles, satisfiabilité et validité
13. Substitutions
13.2. α-renommages
14.1. Forme normale négative
14.2. Forme prénexe

semaine du 20/11

⚠️ QCM₂ en TD, programme : sections 10–13 des notes de cours
TD n°8
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é

semaine du 27/11

MP₂ à rendre pour le 15 décembre
TD n°09
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 04/12

TD n°10
16. Satisfiabilité modulo théorie
16.1.1. Principes de base des solveurs SMT
16.1.2. Élimination des quantificateurs
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.4. Exemple de modélisation : synthèse d'invariant de programme ; fichier SMT-LIB

semaine du 11/12

⚠️ MP₂ à rendre pour le 15/12
TD n°11
17. Calcul des séquents du premier ordre ; Exemple 17.4
17.1. Correction du calcul des séquents du premier ordre

semaine du 18/12

⚠️ pas de cours magistral
TD n°12

Autres ressources pédagogiques

Ouvrages

• Jacques Duparc, La logique pas à pas, Presses polytechniques et universitaires romandes, 2015. catalogue bibliothèques
• John Harrisson, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. catalogue bibliothèques
• René David, Karim Nour et Christophe Raffalli, Introduction à la logique, 2e édition, Dunod, 2003. catalogue bibliothèques
• Jean Goubault-Larrecq et Ian Mackie, Proof Theory and Automated Deduction, volume 6 de Applied Logic Series, Kluwer Academic Publishers, 1997. catalogue bibliothèques

Notes de cours

• Ralf Treinen, Outils logiques, 2012. pdf
• Roberto Amadio, Outils logiques, 2019. pdf
• Sylvain Schmitz, Logique propositionnelle, notes de révision pour l'agrégation, 2018. pdf
• Sylvain Schmitz, Systèmes de preuve, notes de révision pour l'agrégation, 2018. pdf

Années précédentes

• 2022–2023
• 2021–2022
• 2020–2021
• 2019–2020
• 2018–2019