Scribd Logo
Importer

Bienvenue sur Scribd !

  • 448 vues

    TD2 MINC Correction Etudiant

    Transféré par

    kulcan
    Ce document présente la résolution de trois exercices de logique. Le premier exercice montre qu'une formule est universellement valide. Le deuxième exercice formalise des énoncés en logique des prédicats et met la conjonction sous forme clausale. Le troisième exercice montre par résolution avec réfutation que deux propositions découlent de trois autres.

    Droits d'auteur :

    © All Rights Reserved
    Téléchargez comme DOC, PDF, TXT ou lisez en ligne sur Scribd

    TD2 MINC Correction Etudiant

    Transféré par

    kulcan
    448 vues3 pages
    Ce document présente la résolution de trois exercices de logique. Le premier exercice montre qu'une formule est universellement valide. Le deuxième exercice formalise des énoncés en logique des prédicats et met la conjonction sous forme clausale. Le troisième exercice montre par résolution avec réfutation que deux propositions découlent de trois autres.

    Description originale:

    hhkhk

    Copyright

    © © All Rights Reserved

    Formats disponibles

    DOC, PDF, TXT ou lisez en ligne sur Scribd

    Avez-vous trouvé ce document utile ?

    Ce contenu est-il inapproprié ?

    Ce document présente la résolution de trois exercices de logique. Le premier exercice montre qu'une formule est universellement valide. Le deuxième exercice formalise des énoncés en logique des prédicats et met la conjonction sous forme clausale. Le troisième exercice montre par résolution avec réfutation que deux propositions découlent de trois autres.

    Droits d'auteur :

    © All Rights Reserved
    Téléchargez comme DOC, PDF, TXT ou lisez en ligne sur Scribd
    Télécharger au format doc, pdf ou txt
    448 vues3 pages

    TD2 MINC Correction Etudiant

    Transféré par

    kulcan
    Ce document présente la résolution de trois exercices de logique. Le premier exercice montre qu'une formule est universellement valide. Le deuxième exercice formalise des énoncés en logique des prédicats et met la conjonction sous forme clausale. Le troisième exercice montre par résolution avec réfutation que deux propositions découlent de trois autres.

    Droits d'auteur :

    © All Rights Reserved
    Téléchargez comme DOC, PDF, TXT ou lisez en ligne sur Scribd
    Télécharger au format doc, pdf ou txt
    sur 3

    M1- MIAG / MINC 20/02/2007

    TD2 Logique
    Nadia Kabachi

    Exercice 1
    Montrer que
    xy(((U(x) U(y)) T(x)) T(y))
    est universellement valide.
    Correction de lexercice:
    La ngation de la formule prouver est : fx(U(x) T(x)) (U(f(x))
    T(x))
    (T(f(x))). Sous forme clausale, on obtient : C = {U(x1) T(x1), U(f(x2))

    T(x2), T(f(x3))}. On a : H = {fn(a)|n N}.


    En considrant x3 = a, x2 = f(a), x1 = f2(a), et x3 = f(a), on obtient un
    ensemble fini dinstances de base insatisfiable : C = {T(f(a)), U(f2(a))

    T(f(a)),U(f2(a)) T(f2(a)), T(f2(a))}.


    Exercice 2
    Considrons les noncs suivants :
    1. Tous les enfants dun dragon peuvent voler
    2. Archie a au moins un parent vert ou rose
    3. Un dragon est heureux si tous ses enfants peuvent voler
    4. Les dragons verts peuvent voler
    5. Un dragon est vert sil a au moins un parent vert ou rose
    Formaliser les noncs 1 5, puis mettre sous forme clausale la
    conjonction des noncs 3 5.
    Correction de lexercice
    Les noncs proposs se modlisent de la faon suivante. On considre les
    prdicats :
    H(x), x est heureux ; P(x, y), x est parent de y ; V o(x), x peut
    voler ;
    V e(x), x est vert et R(x), x est rose .
    1. xyP(x, y) V o(y)
    2. xP(x,Archie) (V e(x) R(x))
    3 . x(y(P(x, y) V o(y)) H(x))
    4. xV e(x) V o(x)
    5. x((y(P(y, x) (V e(y) R(y))) V e(x))
    On peut remarquer que 5 est quivalent : xy(P(y, x)(V e(y)R(y)))
    V e(x)).

    La mise sous forme clausale des formules considres donne :


    3. Soit F3 = x(y(P(x, y) V o(y)) H(x)).
    F3 x(y(P(x, y) V o(y))) H(x)
    xy((P(x, y) H(x)) (V o(y) H(x)))
    fx((P(x, f(x)) H(x)) (V o(f(x)) H(x)))
    Do`u : CF3 = {P(x1, f(x1)) H(x1), V o(f(x2)) H(x2)}.
    4. Soit F4 = xV e(x) V o(x).
    F4 xV e(x) V o(x)
    Do`u : CF4 = {V e(x3) V o(x3)}.
    5. Soit F5 = x(y(P(y, x) (V e(y) R(y)))) V e(x).
    F5 x((y(P(y, x) (V e(y) R(y)))) V e(x))
    xy(P(y, x) V e(y) V e(x)) (P(y, x) R(y) V e(x))
    Do`u : CF5 = {P(y1, x4) V e(y1) V e(x4), P(y2, x5) R(y2) V
    e(x5)}
    On a donc C = CF3 CF4 CF5 .
    Exercice 3
    Considrons lensemble de propositions suivant :
    1. Un dragon est heureux si tous ses enfants peuvent voler
    2. Les dragons verts peuvent voler
    3. Un dragon est vert sil a au moins un parent vert ou rose
    Montrer par rsolution avec rfutation que :
    4. Les dragons sans enfant sont heureux
    5. Les dragons verts sont heureux
    Correction de lexercice
    Les expressions 1 3 ont t modlises la correction de lexercice 66.
    On a : On
    considre les prdicats : H(x), x est heureux ; P(x, y), x est parent de
    y;
    V o(x), x peut voler ; V e(x), x est vert et R(x), x est rose . La
    forme
    clausale de la conjonction de ces expressions est :
    C = {P(x1, f(x1)) H(x1), V o(f(x2)) H(x2), V e(x3) V o(x3),
    P(y1, x4) V e(y1) V e(x4), P(y2, x5) R(y2) V e(x5)}
    4. Montrons que les dragons sont enfant sont heureux . Une
    modlisation de
    cette expression est :
    x(yP(y, x) H(x))
    La ngation de cette expression est quivalente :
    xyP(y, x) H(x)
    Dont une forme clausale est :
    C4 = {P(b, y), H(a)}
    On a H0 = {a} et H = {{fn(a)|n N}}. On cherche montrer que C
    Cs4
    est insatisfaisable. Nous allons utiliser la rsolution avec rfutation.
    1: C4 P(a, y)
    2: C P(x1, f(x1)) H(x1)

    3:
    4:
    5:
    6:

    subst {a/x1, f(a)/y} {P(a, f(a)), P(a, (a)) H(a)}


    reso H(a)
    C4 H(a)
    reso _

    5. Montrons que les dragons verts sont heureux . Une modlisation de


    cette
    expression est :
    x, V e(x) H(x)
    La ngation de cette expression est quivalente :
    xV e(x) H(x)
    Dont une forme clausale est :
    C5 = {V e(a), H(a)}
    On a H0 = {a} et H = {{fn(a)|n N}}. On cherche montrer que C
    Cs5
    est insatisfaisable. Nous allons utiliser la rsolution avec rfutation.
    1: C5 H(a)
    2: C V o(f(x2)) H(x2)
    3: reso {a/x2} V o(f(a))
    4: C V o(x3) V e(x3)
    5: reso {f(a)/x3} V e(f(a))
    6: C V e(x4) V e(y1) P(y1, x4)
    7: reso {f(a)/x4} V e(y1) P(y1, f(a))
    8: C P(x1, f(x1)) H(x1)
    9: reso {a/x1, a/y1} V e(a) H(a)
    10: C5 H(a)
    11: reso V e(a)
    12: C5 V e(a)
    13: reso _

    Vous aimerez peut-être aussi