Use Modus ponens (A, A -> B |= B) or resolution to show that the following set is inconsistent: 1. Q(x) -> P(x) or not R(a) 2. R(a) or not Q(a) 3. Q(a) 4. not P(a) where x and y are universally quantified variables, a is a constant and P, Q, R are monadic predicates.

GATE 1992 · Discrete Mathematics · Propositional Logic · medium

Answer: Resolution derives the empty clause, so statements 1-4 cannot all hold simultaneously: the set is inconsistent.

1. Convert to clauses and instantiate: Clause 1 Q(x) -> P(x) or not R(a) becomes (not Q(x)) or P(x) or not R(a). Instantiate x = a to get C1a: not Q(a) or P(a) or not R(a). The other clauses are C2: R(a) or not Q(a), C3: Q(a), C4: not P(a).
2. Resolve C1a with Q(a) then not P(a): Resolve C1a with C3 (Q(a)) on the literal Q(a): get P(a) or not R(a). Resolve this with C4 (not P(a)) on P(a): get not R(a).
3. Derive R(a) and close with the empty clause: Resolve C2 (R(a) or not Q(a)) with C3 (Q(a)) to get R(a). Now resolve R(a) with the not R(a) from Step 2 to obtain the empty clause. A derivation of the empty clause means the clause set is unsatisfiable.