The following resolution rule is used in logic programming. Derive clause (P ∨…

GATE · 2003 · CS

Derive clause (P ∨ Q) from clauses (P ∨ R), (Q ∨ ¬R) 

1. A.

   ((P ∨ R) ∧ (Q ∨ ¬R)) ⇒ (P ∨ Q) is logically valid

2. B.

   (P ∨ Q) ⇒ ((P ∨ R)) ∧ (Q ∨ ¬R)) is logically valid

3. C.

   (P ∨ Q) is satisfiable if and only if (P ∨ R) ∧ (Q ∨ ¬R) is satisfiable

4. D.

   (P ∨ Q) ⇒ FALSE if and only if both P and Q are unsatisfiable

Attempted by 153 students.