Corrige UTBM Fondements theoriques de l informatique 2004 GI

Médian MT42 Automne 2004 : Exercice de logiquePablo Gruer26 novembre 20041 Énoncé du problème1.1 Première partieÉtablir l’équivalence logique suivante :A^(B_C) · (A^B)_(A^C)1. par une méthode basée sur la décision2. par une méthode basée sur la déduction1.2 deuxième partieProuver que si U est un ensemble d’axiomes alors T(U) =fF 2 FCP j U † Fg(la théorie de U) est fermée pour la conséquence logique.2 Corrections2.1 Première partieOn constate (théorème 3) queA^(B_C) · (A^B)_(A^C)si et seulement si la formule(A^(B_C)) $ (A^B)_(A^C) (I)est valide. A partir de là,1. méthode basée sur la décision : N’importe quelle méthode de décision de la va-lidité appliquée à la formule (I) : table de vérité, méthode des tableaux, peut servir.1A^(B_C) A^(B_C)E(^) E(^)A [B] A [C]I(^) I(^)A^B A^CI(_) I(_)(A^B)_(A^C) (A^B)_(A^C)A^(B_C)E(^)[B]‘(A^B)_(A^C) [C]‘(A^B)_(A^C) B_CE(_)(A^B)_(A^C)Fig. 1 – Preuve de (II)2. méthode basée sur la déduction : Nous pouvons séparer la formule (I) en deuximplications :(A^(B_C)) ! ((A^B)_(A^C))((A^B)_(A^C))!(A^(B_C))ce qui, du point de vue de la déduction revient aux deux preuves suivantes :A^(B_C) ‘ (A^B)_(A^C) (II)c’est à dire prouver (A^B)_(A^C) avec l’hypothèse A^(B_C) et(A^B)_(A^C)‘A^(B_C) (III)c’est à dire prouver avec A^(B_C) l’hypothèse (A^B)_(A^C).Les preuves de ces propriétés en utilisant la déduction naturelle sont données respec-tivement par les figures 1 et 2. Pour identifier chaque règle utilisée nous ...