Show formally (using a proof rather than a Truth Table) that A follows from the given sentences shown.
- P ∧ Z
- (¬R ∧ ¬W) ∨ (¬P)
- (W ∧ Q) ⇒ P
- Q ∨ W
- Q ⇒ (A ∨ P)
- (P ∧ Q) ⇒ (A ∨ R)
In other words, we need to prove KB ⊨ A, where KB is the collection of sentences. I'll use Resolution Theorem Proving for this proof, and to prove that KB ⊨ A, we need to show that KB ∧ ¬A is unsatisfiable. That is, KB ∧ ¬A is True in NO models.
Resolution Theorem Proving Steps:
Convert KB ∧ ¬A into CNF
- Apply the resolution rule whenever possible and add the result as an additional clause in the conjunction
- Repeat step 2 until either: a. No new clauses can be added: KB does not entail A b. Two clauses resolve to yield the empty clause: KB entails A
Converting the KB to CNF:
Number Sentence
1 P ∧ Z given, already in CNF
1 (P) ∧ (Z) Associativity
2 (¬R ∧ ¬W) ∨ (¬P) Given
2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) Distributivity of ∨ over ∧
3 (W ∧ Q) ⇒ P Given
3 ¬(W ∧ Q) ∨ P Implication elimination
3 (¬W ∨ ¬Q) ∨ P DeMorgan
3 (¬W ∨ ¬Q ∨ P) Associativity, now in CNF
4 Q ∨ W Given
4 (Q ∨ W) Associativity
5 Q ⇒ (A ∨ P) Given
5 ¬Q ∨ (A ∨ P) Implication elimination
5 (¬Q ∨ A ∨ P) Associativity
6 (P ∧ Q) ⇒ (A ∨ R) Given
6 ¬(P ∧ Q) ∨ (A ∨ R) Implication Elimination
6 (¬P ∨ ¬Q) ∨ (A ∨ R) DeMorgan
6 (¬P ∨ ¬Q ∨ A ∨ R) Associativity
7 ¬A Negated query
KB in CNF:
1 (P) ∧ (Z)
2 (¬R ∨ ¬P) ∧ (¬W ∨ ¬P)
3 (¬W ∨ ¬Q ∨ P)
4 (Q ∨ W)
5 (¬Q ∨ A ∨ P)
6 (¬P ∨ ¬Q ∨ A ∨ R)
7 ¬A
I'm stuck at how to come up with a contradiction. Mainly stuck in resolving variables where there are two conjuncts as in (¬R ∨ ¬P) ∧ (¬W ∨ ¬P) (2) and (P) ∧ (Z) (1).
As usual, we have to remove $\land$ and $\to$, using many times Material Implication equivalence as well as Distributivity on 2) to get:
1a) $P$
1b) $Z$
2a) $¬R ∨ ¬P$
2b) $¬W ∨ ¬P$
3) $¬ W ∨ ¬Q ∨ P$
4) $Q ∨ W$
5) $¬Q ∨ A ∨ P$
6) $¬P ∨ ¬Q ∨ A ∨ R$
Now apply Resolution to 1a) and 2a) to get $¬R$ and 1a) and 2b) to get $¬W$.
Use $¬W$ with 4) to get $Q$.
Finally, use $P, Q$ and $¬R$ with 6) to get $A$.