Introduction la logiqueMichel Lvy29 avril 20092Table des matires1Logique propositionnelle7 1.1Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.1.1Formules strictes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.1.2Formules priorit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 1.1.3Notations boolennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2.1Sens des connectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2.2Valeur dune formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 1.2.2.1quivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 1.2.2.2Valide. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 1.2.2.3Modle, Satisfaisable. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 1.2.2.4Consquence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 1.3Les connectives et le langage mathmatique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 1.4Substitution et remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 1.4.1Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 1.4.2Remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 1.5quivalences remarquables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 1.6Algbre de Boole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 1.7Dualit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .15 1.8Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 1.8.1Dfinitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 1.8.2Transformation en sommes de monmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 1.8.2.1Transformation de base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 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.9Fonctions boolennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .18 1.9.1Fonctions boolennes et somme de monmes . . . . . . . . . . . . . . . . . . . . . . . . . .18 1.9.2Fonctions boolennes et produit de clauses. . . . . . . . . . . . . . . . . . . . . . . . . . .19 1.10 Exercices. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .202Rsolution propositionnelle25 2.1Systme de la rsolution. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .25 2.2Compltude du systme de la rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 2.2.1Affectation dun littral . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 2.2.2Compltude de la rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29 2.2.3Restriction de la rsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3Stratgie complte. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3.1Clauses et ensembles de littraux. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 2.3.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.3.2Construction des suites i(i0)et i(i0). . . . . . . . . . . . . . . . . . . . . . .31 2.3.4Clauses minimales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .32 2.4Algorithme de Davis et Putnam . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .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