Logique pour l'informatique

À Ricardo Caferra, mon professeur à l'Ensimag.

Un chapitre de cours et une feuille d'exercices par semaine. Le cours se lit seul ; la feuille se prépare avant la séance de TD, où on la corrige ensemble.

Les six premiers chapitres traitent du calcul propositionnel ; les quatre derniers, de la logique du premier ordre.

Supports de cours

1. Le langage des propositions : Ce qu'est une formule, comment on la lit, et comment on l'écrit avec le moins de parenthèses possible sans changer son sens.
2. Vérité, modèles, conséquence : Donner une valeur de vérité à une formule, classer les formules selon qu'elles peuvent être vraies ou le sont toujours, et dire quand une formule découle d'autres.
3. Formes normales : Ramener toute formule à une forme standard, conjonction de clauses ou disjonction de conjonctions, et ce que ça coûte.
4. Modéliser et résoudre : SAT et énigmes : Traduire un problème en formules, se demander si elles sont cohérentes et ce qu'elles impliquent, et laisser un algorithme chercher la réponse.
5. La résolution : Une seule règle, appliquée à des clauses, qui suffit à montrer qu'un ensemble de formules est contradictoire, et donc qu'une formule découle d'autres.
6. La déduction naturelle : Démontrer une formule par une suite de petits pas, chacun justifié par une règle, comme on raisonne à la main, et pourquoi ces preuves disent vrai.
7. Premier ordre : le langage : Parler des objets et de leurs propriétés avec des termes, des prédicats et des quantificateurs, et savoir quelle variable dépend de quel quantificateur.
8. Premier ordre : sémantique et modélisation : Donner un sens aux formules dans une structure, montrer qu'une formule n'en entraîne pas une autre par un contre-exemple, et traduire le français sans se tromper de quantificateur.
9. Forme prénexe et skolémisation : Sortir tous les quantificateurs en tête, remplacer les « il existe » par des fonctions, et arriver à des clauses, prêtes pour la résolution.
10. Unification et résolution au premier ordre : Trouver la substitution la plus générale qui rend deux termes égaux, s'en servir pour résoudre des clauses avec variables, et ce que la machine peut, ou ne peut pas, décider.

Feuilles d'exercices

1. Lire et écrire des formules : Parenthèses, priorités, arbres de syntaxe, et la frontière entre formules et affirmations sur les formules. Chapitre 1.
2. Vérité, modèles, conséquence : Tables de vérité, modèles, classer une formule, et démontrer des propriétés de la conséquence. Chapitre 2.
3. Formes normales : Mettre en FNC et en FND, par calcul et par table, et exprimer des contraintes avec trois connecteurs seulement. Chapitre 3.
4. Modéliser et résoudre : enquêtes et énigmes : Traduire des faits en formules, tester leur cohérence, faire tourner DPLL à la main, et démêler les habitants de deux îles. Chapitre 4.
5. La résolution : Calculer des résolvantes, réfuter pour prouver une conséquence, et saturer pour montrer qu'un ensemble est satisfiable. Chapitre 5.
6. La déduction naturelle : Écrire des preuves à la Fitch, des plus directes à celles qui demandent le raisonnement par l'absurde, et relier preuve et vérité. Chapitre 6.
7. Premier ordre : le langage : Termes et formules, variables libres et liées, renommage et substitution sans capture. Chapitre 7.
8. Premier ordre : sémantique et modélisation : Évaluer une formule dans une structure, construire des contre-modèles, traduire le français sans ambiguïté, et juger des syllogismes. Chapitre 8.
9. Forme prénexe et skolémisation : Sortir les quantificateurs, les remplacer par des fonctions de Skolem, et passer en clauses. Chapitre 9.
10. Unification et résolution au premier ordre : Calculer des unificateurs les plus généraux, réfuter avec des variables, et suivre ce que fait Prolog. Chapitre 10.