Eléments de logique pour l’informatique
2020–21
http://www.lri.fr/~paulin/Logique
Table des matières
Introduction
Autour de la logique
Programme
Plan
Chapitre 1 Maîtriser le langage logique
1.1 Définition du langage
1.1.1 Objets
1.1.2 Formules atomiques
1.1.3 Formules complexes
1.1.4 Traduire des énoncés en formule logique
1.2 Structure des formules
1.2.1 Représentation des formules comme des arbres
1.2.2 Notations, règles de parenthésage
1.2.3 Variables libres, liées
1.3 Formule vraie
1.3.1 Le cas propositionnel
1.3.2 Formule avec quantificateurs
1.4 Théories et modélisation
1.4.1 Définitions autour des théories
1.4.2 Exemples de théories
1.5 Définition récursive sur les formules
1.5.1 Définir une fonction
1.5.2 Raisonner sur les formules
1.5.3 Définition récursive sur les termes
Chapitre 2 Donner du sens aux formules
2.1 Interprétations et vérité
2.1.1 Définitions
2.1.2 Cas propositionnel
2.1.3 Valeur de vérité d’une formule
2.1.4 Lien entre substitution et valeur de vérité
2.2 Validité et satisfiabilité
2.2.1 Définitions
2.2.2 Substitution et validité
2.3 Conséquence logique, equivalence
2.3.1 Propriétés de la conséquence logique
2.3.2 Equivalences remarquables
2.4 Modèles particuliers
2.4.1 Modèle fini
2.4.2 Modèle de Herbrand
Chapitre 3 Manipuler les formules de la logique
3.1 Formes normales
3.1.1 Forme normale de négation
3.1.2 Clauses
3.1.3 Formes normales conjonctives et disjonctives
3.1.4 Skolémisation
Chapitre 4 Automatiser les démonstrations
4.1 Peut-on automatiser les démonstrations ?
4.1.1 Décidabilité de la logique propositionnelle
4.1.2 Semi-décidabilité de la logique du premier ordre
4.2 Unification
4.2.1 Définitions
4.2.2 Ensemble des solutions
4.2.3 Ordre sur les termes et filtrage
4.3 Résolution
4.3.1 Résolution propositionnelle
4.3.2 Résolution au premier ordre
4.3.3 Questions de stratégie
Conclusion
Annexe A Correction des exercices
A.1 Exercices du chapitre 1
A.2 Exercices du chapitre 2
A.3 Exercices du chapitre 3
A.4 Exercices du chapitre 4