[LO5] Logique 2022–2023

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 : mardi 11:00—13:00 amphi 8C (Sylvain Schmitz)
• travaux dirigés groupe 1 : jeudi 10:45–12:45 halle 278F (Félix Castro)
• travaux dirigés groupe 2 : vendredi 10:45—12:45 salle 1002 (Johan Girardo)
• travaux dirigés groupe 3 : mercredi 14:00—16:00 salle 1005 (Antonio Bucciarelli)
• travaux dirigés groupe 4 : jeudi 10:45—12:45 salle 1003 (Sam Van Gool)
• travaux dirigés groupe 5 : jeudi 16:15—18:15 salle 1005 (Mohammed Foughali)

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
MP₁ à 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 MP₁ à 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

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

MP₂ à rendre pour le 19 décembre
TD n°10
17. Calcul des séquents du premier ordre ; Exemple 17.4
17.1. Correction du calcul des séquents du premier ordre

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.