Les cours auront lieu les jeudis matin de 8h à 10h, et les travaux dirigés les vendredis à 16h. Toutes les séances auront lieu à Beaulieu.
Equipe pédagogique: David Baelde et Maxime Bridoux.
Planning
- 12 janvier: définitions inductives, sémantique du calcul propositionnel, formes normales
- 19 janvier: transformation de Tseitin, problème SAT et variantes
- 26 janvier: compacité, résolution, correction et complétude
- 2 février: variantes de la résolution
- semaine du 6 février: projet algo
- 16 février: déduction naturelle
- (vacances)
- 2 mars: partiel
- 9 mars: logique du premier ordre, syntaxe et sémantique
- 16 mars: théorie des modèles, skolémisation et théorème de Herbrand
- semaine du 20 mars: projet C++
- 30 mars: (in)décidabilité en logique du premier ordre
- 6 avril: complétude de la déduction naturelle
- semaine du 10 avril: projet logique
- (vacances)
- (vacances)
- 4 mai: calcul des séquents
- 9 mai: examen
Documents
- Notes de cours partielles, dernière màj le 16/03
- Devoir à la maison sur la logique propositionnelle, pour le 17/02
- Partiel donné fin février 2023
- Aide mémoire déduction naturelle
- Travaux dirigés: TD1 TD2 TD3 TD4 TD5 TD6 TD7 TD8 TD9 TD10 TD11
Livres
Si besoin, vous pouvez vous référer aux deux livres suivants, le second étant utile surtout pour la déduction naturelle:
- Logique : fondements et applications, Pierre Le Barbenchon, Sophie Pinchinat, François Schwarzentruber. Dunod.
- Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés, Karim Nour, René David, Christophe Raffalli. Dunod.