[LO5] Logique 2024–2025

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 1A (Sylvain Schmitz)
• travaux dirigés groupe 1 : mardi 13:45—15:45 Sophie Germain 1005 (Mohammed Foughali)
• travaux dirigés groupe 2 : lundi 10:45—12:45 Sophie Germain 1005 (Valia Mitsou)
• travaux dirigés groupe 3 : lundi 16:00—18:00 Sophie Germain 1005 (Antonio Bucciarelli)
• travaux dirigés groupe 4 : mercredi 08:30—10:30 Sophie Germain 1003 (Julien Narboux)
• travaux dirigés groupe 5 : vendredi 10:45–12:45 Sophie Germain 1003 (Mohammed Foughali)

Matériel pédagogique

notes de cours ; dernière mise à jour le 24/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.

semaine du 09/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.2. Satisfiabilité et validité

semaine du 16/09

TD n°1
3.1.6. Étendre la syntaxe
3.1.7. Complétude fonctionnelle
4.1. Conséquences logiques
4.2. Équivalences logiques
4.3. Substitutions propositionnelles
4.4. Équivalences usuelles

semaine du 23/09

⚠️ QCM₁ pendant le CM, programme : sections 1–4 des notes de cours
TD n°2
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 30/09

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

semaine du 07/10

choix de binômes
MP₁ à rendre pour le 25/10
TD n°4
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
8. Validité et certificats
8.1. Calcul des séquents propositionnel

semaine du 14/10

TD n°5
7. bonus : Comparaisons des performance des solveurs SAT
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 21/10

⚠️ PA pendant le CM ; durée : 1h, tous documents papiers autorisés, programme : la première partie (sections 1–8 des notes de cours, TD 1–5)
⚠️ MP₁ à rendre pour le 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

semaine du 28/10

🏕️️ semaine de pause

semaine du 04/11

TD n°6
12.1. Sémantique de la logique du premier ordre
12.2. Modèles, satisfiabilité et validité
13. Substitutions

semaine du 11/11

🏕️️️ 11 novembre férié : le CM et les TDs des groupes 2 & 3 sont décalés

semaine du 18/11

⚠️ QCM₂ en TD, programme : sections 10–13 des notes de cours
TD n°07
13.2. α-renommages
14.1. Forme normale négative
14.2. Forme prénexe
15. Théories logiques

semaine du 25/11

TD n°08
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 (non vue en cours)

semaine du 02/12

TD n°09
TD n°10
MP₂ à rendre pour le 17/12
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.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 09/12

TD n°11
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

semaine du 16/12

⚠️ MP₂ à rendre pour le 17/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

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