En utilisant le petit programme d'aide a la preuve en déeduction
naturelle suivant : deptinfo.cnam.fr/~ponso/SOFTS/deduction1.html
prouver les formules suivantes (~ represente non).



1 p /\ q => q /\ p

2 p /\ (q /\ r) => (p /\ q) /\ r

3 ( (p /\ q) /\ r)  => p /\ (q /\ r)

4 p /\ (q /\ r) <=> (p /\ q) /\ r (a vous d'encoder <=> grace a => et /\)

5 p \/ q => q \/ p

6 (p \/ (q \/ r) => (p \/ q) \/ r )  

7  (p \/ q) \/ r => p \/ (q \/ r) 

8 (p /\ (q \/ r) => (p /\ q) \/ (p /\ r))

9 (p \/ (q /\ r) => (p \/ q) /\ (p \/ r))

10 (p => q) /\ (q => r) => (p => r)

11 ((p /\ q => r) => (p => (q => r)))

12 ((p \/ q => r) => (p => r) /\ (q => r)) /\( (p => r) /\ (q => r) => (p \/ q => r) )

13 (p => ~ ~ p)/\ (p <= ~ ~ p)

14 (p => q) => (~ q => ~ p)

15 (~ q => ~ p) => (p => q)

16 ~ (p \/ q) <=> ~ p /\ ~ q   (a vous d'encoder <=> grace a => et /\)

17 ~ (p /\ q) <=> ~ p \/ ~ q  (a vous d'encoder <=> grace a => et /\)

18 ~ (p => q) <=> p /\ ~ q    (a vous d'encoder <=> grace a => et /\)