TP 4 : Résolution

Quel est le résolvant des paires de clauses suivantes :

1. (x∨y∨z) et (¬x∨y∨w).
2. (x∨¬y∨z) et (¬x∨y∨w).
3. (¬x∨¬y∨z) et (¬x∨¬y∨w).

Soit F = (p⇒q) ∧ (r⇒¬q) ∧ (q⇒r). Prouvez, en utilisant la résolution, que F ⊨ ¬p.

Donner une réfutation par résolution de la formule suivante :

(p_1, 1∨p_1, 2) ∧ (p_2, 1∨p_2, 2) ∧ (p_3, 1∨p_3, 2) ∧ (¬p_1, 1∨¬p_2, 1) ∧ (¬p_1, 1∨¬p_3, 1) ∧ (¬p_2, 1∨¬p_3, 1) ∧ (¬p_1, 2∨¬p_2, 2) ∧ (¬p_1, 2∨¬p_3, 2) ∧ (¬p_2, 2∨¬p_3, 2)