Logiques
L'UE compte 30h d'enseignement pour 3 ECTS.
Nous utiliserons essentiellement les documents rédigés par
Stéphane Devismes,
Emmanuel Filiot,
Pascal Lafourcade,
Michel Lévy et
Benjamin Wack ainsi que les logiciels
FitchJS de Michael Rieppel et
Logictools de Tanel Tammet.
Je remercie chaleureusement ces collègues pour leur générosité !
Chaque séance comporte une partie cours et une partie TD où nous utiliserons nos ordinateurs.
Tous les documents nécessaires à la réussite de cette UE sont disponibles à partir de cette page.
Plan
- Logique propositionnelle
- Syntaxe et sémantique
- Tables de vérité, formes normales
- Déduction naturelle
- Logique du premier ordre
- Syntaxe et sémantique
- Déduction naturelle
Organisation hebdomadaire
- séance 1
- cours/td : 1,
intro déduction naturelle via FitchJS,
exercices introductifs de déduction naturelle en logique propositionnelle
- pour la prochaine séance : refaire tous les exercices du jour avec et sans FitchJS
- séance 2
- cours/td : fin de 1, que se passe-t-il si des hypothèses sont contradictoires ou si
une hypothèse est fausse ?
Déduction naturelle en FitchJS via les
exercices introductifs de déduction naturelle en logique propositionnelle,
- pour la prochaine séance : exercices 1-10 p. 35-36 du polycopié, avancer sur les
exercices introductifs de déduction naturelle en logique propositionnelle
- séance 3
- cours/td : 2 et 3,
exemples de formes normales, correction exercices 6-10 p. 35-36,
déduction naturelle via FitchJS,
exercices introductifs de déduction naturelle en logique propositionnelle
- pour la prochaine séance : exercices 20 et 21 p. 37-38 du polycopié,
exercices 3, 4 et 5 sur les formes normales,
FitchJS : terminer cette fiche et démarrer celle-ci
- séance 4
- cours/td : correction de l'exercice 20 p. 37 du polycopié,
de l'exercice 3 sur les formes normales et
des premiers exercices de cette fiche
- pour la prochaine séance : réviser les 4 premières séances
- séance 5
- contrôle continu et correction
- cours/td : 7 et
indécidabilité de la logique du premier ordre : 9
-
pour la prochaine séance : préparer les exercices 63, 64, 67, 68 et 69 p. 100 et 101 du polycopié
- séance 6
- cours/td : 7, correction de l'exercice 63,
FitchJS : exercices de déduction naturelle en logique du premier ordre
- pour la prochaine séance : exercices 64, 67, 68 et 69 p. 101, exercices de déduction naturelle en logique du premier ordre
- séance 7
- cours/td : 8 et 9, correction des exercices
64, 67, 68 et 69 p. 101, exercices de déduction naturelle
en logique du premier ordre
- pour la prochaine séance : exercices de déduction naturelle en logique du premier ordre
- séance 8 de 2h (puis cours Vérification 2h)
- exercices de déduction naturelle
en logique du premier ordre, correction du partiel de l'année précédente
- contrôle terminal
Documents
- Le polycopié
- Exercices introductifs de déduction naturelle en logique propositionnelle
- Exercices de déduction naturelle en logique propositionnelle
- Exercices de déduction naturelle en logique du premier ordre
Evaluation
Contrôle continu : une interrogation et un contrôle terminal écrit, tous deux sans document ni moyen électronique, 50% + 50%
Deuxième session : examen écrit sans document ni moyen électronique, tout est au programme, 100%
Au programme du premier contrôle écrit :
- Logique propositionnelle
- Toutes les définitions, tous les énoncés de propriétés/lemmes/théorèmes, tous les algorithmes et tous les exercices vus ensemble,
y compris la déduction naturelle
- Enoncé et démonstration de la propriété 1.2.27 : conséquence logique, validité et insatisfiabilité
- Familiarité avec la déduction naturelle et le format de preuve Fitch
- Enoncés : décidabilité de la validité, correction de la déduction naturelle, complétude de la déduction naturelle
Au programme du second contrôle écrit :
- Logique du premier ordre
- Définitions : signature, terme, formule atomique, formule, signature associée,
variable libre, variable liée, interprétation, satisfiabilité, modèle, contre-modèle, validité
- Tous les exercices vus ensemble
- Familiarité avec la manipulation des quantificateurs, la déduction naturelle et le format de preuve Fitch
- Enoncés : indécidabilité de la validité, correction de la déduction naturelle, complétude de la déduction naturelle
Annales
Ressources
Bibliographie
- Informatique théorique : logique et démonstration automatique
Michel Lévy, Stéphane Devismes et Pascal Lafourcade, Ellipses, 2012
- Initiation à la logique formelle, T. Lucas, I. Berlanger, I. De Greef, Editions De Boeck, 2007
- Logic in Computer Science: Modeling and Reasoning about Systems,
M. Huth and M. Ryan, Cambridge University Press, 2004
- Mathematical Logic for Computer Science, M. Ben-Ari, Springer, 2012
