Devoirs Hebdomadaire N°3
CDL...DH3
p :- k,a. p :- b. k :- d. k. a :- d,c. a :- e. b. d :- e. d. |
QUESTION 1 : donner la base de Herbrand de ce programme et construire sa sémantique en chaînage avant (sémantique de point fixe, vous pouvez vous servir de l'applet Travaux Pratiques ProPlog)
QUESTION 2 : donner la forme clausale FC de ce programme.
QUESTION 3 : prouverz FC |- p par réfutation/résolution selon la stratégie Prolog, puis par une suite de résolutions plus efficace (moins de pas de calcul).
QUESTION 4 : prouver FC |= p par réfutation/raisonnement .
QUESTION 5 : prouverFC |- p sur un tableau sémantique.
QUESTION 6 : justifier par une phrase l'inutilité des clauses : k :- d. et d :- e. (chaînage arrière).
Soit le programme ProPlog dh03_1.pl :
| p :- k,a. p :- b. k :- d. k. a :- d,c. a :- e. b. d :- e. d. |
Question n°1
La base de Herbrand est l'ensemble des atomes utilisés dans le programme :
Bp = {a, b, c, d, e, p, k}
Sémantique en chaînage avant :
| Tp1 = {b,k,d} Tp2 = {b,k,p,d} Tp3 = {b,k,p,d} denotation: {b,k,d,p} |
Question n°2
Forme clausale FC du programme.
FC = ((k&a) -> p) & (b -> p) & (d -> k) & k & ((d&c) -> a) & (e -> a) & b & (e -> d) & d
FC = (~(k&a) v p) & (~b v p) & (~d v k) & k & (~(d&c) v a) & (~e v a) & b & (~e v d) & d
FC = (~k v ~a v p) & (~b v p) & (~d v k) & k & (~d v ~c v a) & (~e v a) & b & (~e v d) & d
Question n°3
Prouvons que FC |- p par réfutation/résolution selon la stratégie Prolog.
Ensemble contradictoire : {~k v ~a v p , ~b v p , ~d v k , k , ~d v ~c v a , ~e v a , b , ~e v d , d, ~p}
On calcule les résolvantes qui ont un parent dans l'ensemble de départ :
|
~k v ~a v p
|
~b v p
|
~d v k
|
k
|
~d v ~c v a
|
~e v a
|
b
|
~e v d
|
d
|
~p
|
|
1
|
2
|
3
|
4
|
5
|
6
|
7
|
8
|
9
|
10
|
1 + 10 = ~k v ~a -> 11
11 + 3 = ~a v ~d -> 12
12 + 9 = ~a -> 13
13 + 6 = ~e -> 14
Pour démontrer ~e il faut ajouter e à l'énoncé donc l'ensemble est bien contradictoire.
Autre manière en prenant une suite de résolutions plus efficace :
Ensemble contradictoire : {~k v ~a v p , ~b v p , ~d v k , k , ~d v ~c v a , ~e v a , b , ~e v d , d, ~p}
~p + ~b v p -> ~b
~b + b -> Faux
Question n°4
Prouvons FC |= p par réfutation/raisonnement.
On cherche une conclusion fausse alors que les hypothèses vraies.
|
(~k v ~a v p) ,
|
(~b v p) ,
|
(~d v k) ,
|
k ,
|
(~d v ~c v a) ,
|
(~e v a) ,
|
b ,
|
(~e v d) ,
|
d
|
|=
|
p
|
|
T
|
T
|
T
|
T
|
T
|
T
|
T
|
T
|
T
|
|
F
|
|
1
|
2
|
3
|
4
|
5
|
6
|
7
|
8
|
9
|
|
10
|
|
b = T d'après 7
p = F d'après 10 ~b v p = ~T v F ~b v p = F v F ~b v p = F Impossible |
Question n°5
Prouvons FC |- p sur un tableau sémantique.
Tous les chemins sont fermés.
Question n°6
Inutilité des clauses (chaînage arrière) :
k :- d. et d :- e.
k et d sont dans la dénotation du programme, ce sont des faits.
FIN_dh3
ACCUEIL CONTACT FAVORIS ANNALES DH1 DH2 DH3 DH4 DH5 DH6 DH7 DH8 DH9 DH10 DH11 DH12 DH13 DH14 DH15 DH16