Contrôle LPL CP1 du 19/12/2018 - Corrigé

Question 1.

(i) On prend les interprétations de A et B toujours vraies:
I(A)(0) = I(A)(1) = I(B)(0) = I(B)(1) = V.
Alors I(A)(x), I(B)(x) et I(A)(x) v I(B)(x) sont vrais pour tout x dans E, donc (a) et (b) donnent tous deux "vrai".

(ii) On prend les interprétations de A et B toujours fausses:
I(A)(0) = I(A)(1) = I(B)(0) = I(B)(1) = F.
Alors I(A)(x), I(B)(x) et I(A)(x) v I(B)(x) sont faux pour tout x dans E, donc (a) et (b) donnent tous deux "faux".

(iii) On prend les interprétations de A et B signifiant respectivement "est pair" et "est impair":
I(A)(0) = I(B)(1) = V, I(A)(1) = I(B)(0) = F.
Comme I(A)(1) = F, l'interprétation de "pourtout x A(x)" est "faux", de même comme I(B)(0) = F, l'interprétation de "pourtout x B(x)" est "faux". Donc (b) donne "faux".
Comme I(A)(0) v I(A)(1) = I(B)(0) v I(B)(1) = V, (a) donne "vrai".

(iv) Non, d'après le paragraphe (4) de "Mise en forme des formules", (a) est une conséquence de (b), donc quand (b) est vrai, alors (a) est vrai (ce qui est d'ailleurs facile à montrer).

Question 2.
J'écris v, ^, =>, -- pour ou, et, implique, non.
Prédicats:
bel(x): x est belge.
fri(x): x mange des frites.
fum(x): x est fumeur.
vin(x): x boit du vin.
san(x): x est en bonne santé.

Traduction de l'énoncé en formules:
(i)   PourTout x (bel(x) => fri(x))
(ii)  PourTout x ((fri(x) ^ --fum(x)) => san(x))
(iii) PourTout x (vin(x) => --fum(x))
(iv)  IlExiste x (bel(x) ^ --san(x))
(c)   IlExiste x (--vin(x) ^ fri(x))

(i,ii,iii,iv) sont sous forme prénexe; voici --(c) sous forme prénexe:
--(c) PourTout x --(--vin(x) ^ fri(x))
Pour skolemiser, on enlève le "PourTout x" dans (i,ii,iii) et --(c), tandis que dans (iv) on enlève le "IlExiste x" et on remplace la variable x par une constante a.
En remplaçant X => Y par --X v Y et --(X ^ Y) par (--X v --Y), on obtient:
(1) --bel(x) v fri (x)
(2) --fri(x) v fum(x) v san(x)
(3) --vin(x) v --fum(x)
(4) bel(a) ^ --san(a), a constante, ce qui donne deux clauses
    (4a) bel(a)
    (4b) --san(a)
(5) vin(x) v --fri(x)

Résolution:
(1) & (4a) [x <- a]
--bel(x) v fri (x), bel(a) |- fri(a) (6)
(2) & (6) [x <- a]
--fri(x) v fum(x) v san(x), fri(a) |- fum(a) v san(a) (7)
(7) & (4b)
fum(a) v san(a), --san(a) |- fum(a) (8)
(3) & (8) [x <- a]
--vin(x) v --fum(x), fum(a) |- --vin(a) (9)
(5) & (9) [x <- a]
vin(x) v --fri(x), --vin(a) |- --fri(a) (10)
(6) & (10)
fri(a), --fri(a) |- clause vide