Une page de Wikiversité, la communauté pédagogique libre.
En raison de limitations techniques, la typographie souhaitable du titre, «
Exercice : Cohérence et formes clausalesLogique (mathématiques)/Exercices/Cohérence et formes clausales », n'a pu être restituée correctement ci-dessus.
Voici 2 types d'exercices pour les formes clausales.
Soit la conséquence suivante :
⊨
(
(
p
→
q
)
∨
(
r
→
s
)
)
→
(
p
∧
r
→
q
∨
s
)
{\displaystyle \models ((p\rightarrow q)\lor (r\rightarrow s))\rightarrow (p\land r\rightarrow q\lor s)}
.
Est-elle vraie ? Prouvez-le en utilisant la méthode de résolution (appliquée aux formes clausales).
Solution
Nous simplifions la conséquence en enlevant les implications :
⊨
(
(
p
→
q
)
∨
(
r
→
s
)
)
→
(
p
∧
r
→
q
∨
s
)
⊨
¬
(
(
¬
p
∨
q
)
∨
(
¬
r
∨
s
)
)
∨
(
¬
(
p
∧
r
)
∨
q
∨
s
)
⊨
¬
(
¬
p
∨
q
∨
¬
r
∨
s
)
∨
(
¬
p
∨
¬
r
∨
q
∨
s
)
⊨
(
p
∧
¬
q
∧
r
∧
¬
s
)
∨
¬
p
∨
¬
r
∨
q
∨
s
{\displaystyle {\begin{aligned}&\models ((p\rightarrow q)\lor (r\rightarrow s))\rightarrow (p\land r\rightarrow q\lor s)\\&\models \neg ((\neg p\lor q)\lor (\neg r\lor s))\lor (\neg (p\land r)\lor q\lor s)\\&\models \neg (\neg p\lor q\lor \neg r\lor s)\lor (\neg p\lor \neg r\lor q\lor s)\\&\models (p\land \neg q\land r\land \neg s)\lor \neg p\lor \neg r\lor q\lor s\\\end{aligned}}}
Nous prenons la négation de la conséquence, on arrive donc à :
⊨
(
¬
p
∨
q
∨
¬
r
∨
s
)
∧
p
∧
r
∧
¬
q
∧
¬
s
{\displaystyle \models (\neg p\lor q\lor \neg r\lor s)\land p\land r\land \neg q\land \neg s}
Nous avons donc 5 clauses que l’on retrouve du point 1 à 5.
1.
¬
p
∨
q
∨
¬
r
∨
s
2.
p
3.
r
4.
¬
q
5.
¬
s
6.
q
∨
¬
r
∨
s
(
1
,
2
)
7.
¬
r
∨
s
(
4
,
6
)
8.
s
(
3
,
7
)
9.
◻
(
5
,
8
)
{\displaystyle {\begin{aligned}&1.\neg p\lor q\lor \neg r\lor s\\&2.p\\&3.r\\&4.\neg q\\&5.\neg s\\&6.q\lor \neg r\lor s\qquad (1,2)\\&7.\neg r\lor s\qquad (4,6)\\&8.s\qquad (3,7)\\&9.\Box \qquad (5,8)\\\end{aligned}}}
La conséquence est donc vraie.
Soit la conséquence suivante :
⊨
(
a
∧
b
∨
c
∧
d
)
∧
(
a
→
¬
a
)
∧
¬
c
{\displaystyle \models (a\land b\lor c\land d)\land (a\rightarrow \neg a)\land \neg c}
.
Est-elle vraie ? Prouvez-le en utilisant la méthode de résolution (appliquée aux formes clausales).
Solution
Nous simplifions la conséquence en enlevant les implications :
⊨
(
a
∧
b
∨
c
∧
d
)
∧
(
a
→
¬
a
)
∧
¬
c
⊨
(
a
∨
c
∧
a
∨
d
∧
b
∨
c
∧
b
∨
d
)
∧
(
¬
a
∨
¬
a
)
∧
¬
c
⊨
(
a
∨
c
∧
a
∨
d
∧
b
∨
c
∧
b
∨
d
)
∧
¬
a
∧
¬
c
{\displaystyle {\begin{aligned}&\models (a\land b\lor c\land d)\land (a\rightarrow \neg a)\land \neg c\\&\models (a\lor c\land a\lor d\land b\lor c\land b\lor d)\land (\neg a\lor \neg a)\land \neg c\\&\models (a\lor c\land a\lor d\land b\lor c\land b\lor d)\land \neg a\land \neg c\\\end{aligned}}}
Nous montrons sa contradiction, donc nous n'avons pas besoin de la négation de la conséquence.
On a donc 6 clauses que l’on retrouve du point 1 à 6.
1.
a
∨
c
2.
a
∨
d
3.
b
∨
c
4.
b
∨
d
5.
¬
a
6.
¬
c
7.
c
(
1
,
5
)
8.
◻
(
6
,
7
)
{\displaystyle {\begin{aligned}&1.a\lor c\\&2.a\lor d\\&3.b\lor c\\&4.b\lor d\\&5.\neg a\\&6.\neg c\\&7.c\qquad (1,5)\\&8.\Box \qquad (6,7)\\\end{aligned}}}
La contradiction est vraie, donc la conséquence est fausse.