|
| Titre : | Logique et démonstration automatique [Texte imprimé] : introduction à la logique propositionnelle et à la logique du premier ordre | | Type de document : | texte imprime | | Auteurs : | Stéphane Devismes ; Michel Lévy Pascal Lafourcade | | Editeur : | Paris : Ellipses | | Année de publication : | 2012 | | Collection : | Technosup (Paris), 1275-3955 | | Importance : | 209 p. | | Présentation : | fig., tabl., couv. ill. | | Format : | 26 cm | | ISBN/ISSN/EAN : | 978-2-7298-7229-8 | | Note générale : | Bibliogr. p. [205]. Index | | Langues : | Français | | Mots-clés : | Logique du premier ordre Calcul des propositions Boole, Algèbre de Théorèmes :démonstration automatique Algorithmes | | Résumé : | Une étude limitée à la logique classique à deux valeurs de vérité (logique qui est celle des circuits combinatoires) pour renforcer rigueur de raisonnement et conforter l'aptitude à raisonner, avec de nombreux exercices corrigés gradués | | Note de contenu : | Table des matières
A Logique propositionnelle...........................5
I Logique propositionnelle...........................7
1 Syntaxe.................................................... 8
2 Sens des formules............................................... 11
3 Substitution et remplacement......................................... 17
4 Formes Normales............................................... 19
5 Algèbre de Boole............................................... 21
6 Fonctions booléennes............................................. 25
7 Circuits.................................................... 27
8 L’outil BDDC................................................. 29
9 Exercices................................................... 31
II Résolution propositionnelle....................................37
1 Résolution................................................... 38
2 Stratégie complète.............................................. 46
3 Algorithme de Davis-Putnam-Logemann-Loveland............................. 55
4 Transformation en temps linéaire d’une formule en produit de clauses................... 60
5 Exercices................................................... 66
III Déduction Naturelle...........................................71
1 Système formel de la déduction naturelle................................... 72
2 Tactiques de preuve.............................................. 77
3 Cohérence de la déduction naturelle..................................... 79
4 Complétude de la déduction naturelle.................................... 79
5 Outils..................................................... 81
6 Exercices................................................... 83
B Logique du premier ordre.......................................85
IV Logique du premier ordre........................................87
1 Syntaxe.................................................... 88
2 Être libre ou lié................................................ 90
3 Sens des formules............................................... 91
4 Équivalences remarquables.......................................... 99
5 Exercices...................................................102
V Base de la démonstration automatique..........................107
1 Méthodes de Herbrand............................................108
2 Skolémisation.................................................112
3 Unification..................................................117
4 Résolution au premier ordre.........................................120
5 Exercices...................................................126
4Table des matières
VI Déduction naturelle au premier ordre : quantificateurs, copie et égalité
129
1 Règles pour la logique du premier ordre...................................129
2 Tactiques de preuves.............................................133
3 Cohérence du système............................................135
4 Exercices...................................................138
C Annexes.......................................................141
Corrigés.........................................................143
Bibliographie....................................................205
Index............................................................207 | | En ligne : | http://www.editions-ellipses.fr/PDF/9782729872298_extrait.pdf | | Permalink : | ./index.php?lvl=notice_display&id=9602 |
Logique et démonstration automatique [Texte imprimé] : introduction à la logique propositionnelle et à la logique du premier ordre [texte imprime] / Stéphane Devismes ; Michel Lévy Pascal Lafourcade . - Paris : Ellipses, 2012 . - 209 p. : fig., tabl., couv. ill. ; 26 cm. - ( Technosup (Paris), 1275-3955) . ISBN : 978-2-7298-7229-8 Bibliogr. p. [205]. Index Langues : Français | Mots-clés : | Logique du premier ordre Calcul des propositions Boole, Algèbre de Théorèmes :démonstration automatique Algorithmes | | Résumé : | Une étude limitée à la logique classique à deux valeurs de vérité (logique qui est celle des circuits combinatoires) pour renforcer rigueur de raisonnement et conforter l'aptitude à raisonner, avec de nombreux exercices corrigés gradués | | Note de contenu : | Table des matières
A Logique propositionnelle...........................5
I Logique propositionnelle...........................7
1 Syntaxe.................................................... 8
2 Sens des formules............................................... 11
3 Substitution et remplacement......................................... 17
4 Formes Normales............................................... 19
5 Algèbre de Boole............................................... 21
6 Fonctions booléennes............................................. 25
7 Circuits.................................................... 27
8 L’outil BDDC................................................. 29
9 Exercices................................................... 31
II Résolution propositionnelle....................................37
1 Résolution................................................... 38
2 Stratégie complète.............................................. 46
3 Algorithme de Davis-Putnam-Logemann-Loveland............................. 55
4 Transformation en temps linéaire d’une formule en produit de clauses................... 60
5 Exercices................................................... 66
III Déduction Naturelle...........................................71
1 Système formel de la déduction naturelle................................... 72
2 Tactiques de preuve.............................................. 77
3 Cohérence de la déduction naturelle..................................... 79
4 Complétude de la déduction naturelle.................................... 79
5 Outils..................................................... 81
6 Exercices................................................... 83
B Logique du premier ordre.......................................85
IV Logique du premier ordre........................................87
1 Syntaxe.................................................... 88
2 Être libre ou lié................................................ 90
3 Sens des formules............................................... 91
4 Équivalences remarquables.......................................... 99
5 Exercices...................................................102
V Base de la démonstration automatique..........................107
1 Méthodes de Herbrand............................................108
2 Skolémisation.................................................112
3 Unification..................................................117
4 Résolution au premier ordre.........................................120
5 Exercices...................................................126
4Table des matières
VI Déduction naturelle au premier ordre : quantificateurs, copie et égalité
129
1 Règles pour la logique du premier ordre...................................129
2 Tactiques de preuves.............................................133
3 Cohérence du système............................................135
4 Exercices...................................................138
C Annexes.......................................................141
Corrigés.........................................................143
Bibliographie....................................................205
Index............................................................207 | | En ligne : | http://www.editions-ellipses.fr/PDF/9782729872298_extrait.pdf | | Permalink : | ./index.php?lvl=notice_display&id=9602 |
|  |
Logique et démonstration automatique [Texte imprimé] (2012) 
