[LO5] Logique 2021–2022

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 15% de la note finale
• DM₁, DM₂ : deux devoirs (maison ou sous forme d'examens en présentiel selon possibilités), chacun 25% de la note finale

Séances et intervenant·e·s

• cours magistraux : mercredi 10:45—12:45 amphi 1A (Sylvain Schmitz)
• travaux dirigés groupe 1 : mardi 08:30—10:30 salle 1005 (Antonio Bucciarelli)
• travaux dirigés groupe 2 : lundi 14:00–16:00 salle 2036 (Mohammed Foughali)
• travaux dirigés groupe 3 : jeudi 10:45—12:45 salle 1008 (Daniela Petrisan)
• travaux dirigés groupe 4 : vendredi 10:45—12:45 salle 2036 (Sam van Gool)
• travaux dirigés groupe 5 : lundi 10:45—12:45 salle 2003 (Florian Horn)

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 30/11.

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; correction exo 4 (a), exo 4 (b–c), exo 4 (d–e)
MP₁ à 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

TD n°6
DM₁ à rendre pour le 12 novembre
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 29 octobre

semaine du 01/11

vacances

semaine du 08/11

⚠️ amphi en salle 2A
TD n°7
12.2. Modèles, satisfiabilité et validité
13. Substitutions
13.2. α-renommages
⚠️ ne pas oublier le DM₁ à rendre pour le 12 novembre

semaine du 15/11

TD n°8
14.1. Forme normale négative
14.2. Forme prénexe
14.3. Skolémisation

semaine du 22/11

⚠️ QCM₂ à 10:45 le 24/11 en amphi 1A
TD n°09
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

TD n°10
MP₂ à rendre pour le 17 décembre
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 06/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
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
TD n°12
⚠️ ne pas oublier le MP₂ à rendre pour le 17 décembre

semaine du 03/01

⚠️ DM₂ en examen présentiel le 05/01/2022, 12:00–14:00 en salles 11E - 12E - 7C & 3B. Au programme, sections 10 à 17 des notes de cours et TD n°7 à 12. Tous documents papier autorisés. en distanciel à rendre pour le 20 janvier