0
$\begingroup$

Show formally (using a proof rather than a Truth Table) that A follows from the given sentences shown.

  1. P ∧ Z
  2. (¬R ∧ ¬W) ∨ (¬P)
  3. (W ∧ Q) ⇒ P
  4. Q ∨ W
  5. Q ⇒ (A ∨ P)
  6. (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

  1. Apply the resolution rule whenever possible and add the result as an additional clause in the conjunction
  2. 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).

$\endgroup$

1 Answer 1

1
$\begingroup$

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$

7) $¬A$


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$.

$\endgroup$
2
  • $\begingroup$ Is it allowed to use the same sentence, say 1a, twice to form new sentences? $\endgroup$ Mar 18, 2019 at 15:33
  • $\begingroup$ @LeonardoLopez - the Resolution proof procedure is aimed at automated theorem proving (i.e. to be performed by a machine) : "The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals." $\endgroup$ Mar 18, 2019 at 15:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .