Logique mathématique et calculabilité

Table des matières / Sommaire :

1 Rappels mathématiques
Les entiers naturels – 2
Induction mathématique – 3
Démonstration par l’absurde – 5
Démonstration par contradiction – 6
Travaux dirigés – 8
2 Calcul propositionnel
2.1 Préliminaires – 10
2.1.1 Définition des connecteurs →, ¬, ∧ et ∨ – 11
2.2 Syntaxe du langage de la logique propositionnelle – 14
2.3 Sémantique de la logique propositionnelle – 14
2.4 Théorème de remplacement – 16
2.5 Forme normale conjonctive – 19
2.6 Ensemble complet de connecteurs – 21
2.7 Travaux dirigés – 25
3 Calcul propositionnel formel
3.1 Système déductif pour le calcul propositionnel – 28
3.2 Adéquation et complétude du CPF – 34
3.3 Méthode de Davis–Putnam – 38
3.4 Calcul des séquents – 41
3.5 Travaux dirigés – 45
4 Calcul des prédicats du premier ordre
4.1 Langage du calcul des prédicats – 48
4.2 Variables libres et variables liées – 49
4.3 Interprétation – 50
4.4 Satisfaction, valeurs de vérité – 51
4.5 Calcul des prédicats formalisé – 53
4.6 Forme normale prénexe – 62
4.7 Solémisation et résolution – 64
4.7.1 Formes clausales, skolémisation – 65
4.7.2 Procédure de Herbrand – 68
4.7.3 Méthode de résolution, unification – 70
5 Notions de calculabilité
5.1 Introduction – 82
5.2 Notion de calcul effectif et d’algorithme – 82
5.3 Fonctions récursives – 83
5.4 Machines de Turing – 89
5.4.1 Les machines de Turing – 89
5.4.2 Concaténation de machines – 93
5.5 Travaux dirigés – 97
6 λ-Calcul et logique combinatoire
6.1 Le lambda-calcul – 100
6.1.1 λβ-réduction, λβ-conversion – 100
6.1.2 βη-réduction – 102
6.2 La logique combinatoire – 103
6.2.1 Réduction faible, égalité faible – 103
6.2.2 Abstraction – 104
6.2.3 Cβη-réduction et extensionnalité – 105
6.3 Représentation des fonctions récursives – 106
6.4 Travaux dirigés – 109
Annexe
A.1 Correction des exercices du chapitre 1 – 111
A.2 Correction des exercices du chapitre 2 – 112
A.3 Correction des exercices du chapitre 3 – 113
A.4 Correction des exercices du chapitre 4 – 115
A.5 Correction des exercices du chapitre 5 – 117
A.6 Correction des exercices du chapitre 6 – 118