《程序逻辑(法语)》由会员分享，可在线阅读，更多相关《程序逻辑(法语)（95页珍藏版）》请在金锄头文库上搜索。
1、Introduction la logiqueMichel Lvy29 avril 20092Table des matires1Logique propositionnelle7 1.1Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.1.1Formules strictes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2、. . . .8 1.1.2Formules priorit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.1.3Notations boolennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3、 . . . . . . . . . . . . .9 1.2.1Sens des connectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2.2Valeur dune formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2.2.1quivalence . . . . . . . . . . . . . . . . . . . . . . .
4、 . . . . . . . . . . . . . . .10 1.2.2.2Valide. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 1.2.2.3Modle, Satisfaisable. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 1.2.2.4Consquence . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5、 . . . . . . . . .11 1.3Les connectives et le langage mathmatique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 1.4Substitution et remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 1.4.1Substitution . . . . . . . . . . . . . . . . . . . .
6、. . . . . . . . . . . . . . . . . . . . . . . .12 1.4.2Remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 1.5quivalences remarquables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 1.6Algbre de Boole . . . . . . . . .
7、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 1.7Dualit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 1.8Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16
8、1.8.1Dfinitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 1.8.2Transformation en sommes de monmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 1.8.2.1Transformation de base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16
9、 1.8.2.2Ordre des transformations et simplifications. . . . . . . . . . . . . . . . . . . . .17 1.8.3Utilisation des sommes de monmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .17 1.8.4Transformation en produit de sommes de littraux. . . . . . . . . . . . . . . . . . . . . . .17 1.
10、9Fonctions boolennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .18 1.9.1Fonctions boolennes et somme de monmes . . . . . . . . . . . . . . . . . . . . . . . . . .18 1.9.2Fonctions boolennes et produit de clauses. . . . . . . . . . . . . . . . . . . . . . . .
11、 . . .19 1.10 Exercices. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .202Rsolution propositionnelle25 2.1Systme de la rsolution. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .25 2.2Compltude du systme de la rsolution
12、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 2.2.1Affectation dun littral . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 2.2.2Compltude de la rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29 2.2.3Restriction de la
13、 rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3Stratgie complte. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3.1Clauses et ensembles de littraux. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3
14、.2Rduction dun ensemble de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3032.3.3Construction de toutes les clauses dduites dun ensemble de clauses. . . . . . . . . . . . .31 2.3.3.1Plan de la construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .31 2.3
15、.3.2Construction des suites i(i0)et i(i0). . . . . . . . . . . . . . . . . . . . . . .31 2.3.4Clauses minimales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .32 2.4Algorithme de Davis et Putnam . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
16、 .33 2.4.1Suppression des clauses qui ont des littraux isols . . . . . . . . . . . . . . . . . . . . . . .33 2.4.2Rsolution unitaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34 2.4.3Algorithme de Davis et Putnam. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34 2.5Exercices. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .373Dduction Naturelle39
