I need to prove $\{P \vee (Q \wedge R), S \} \models (S \wedge P) \vee Q$ using resolution theorem or resolution refutation. This is my proof:

  1. Convert $P \vee (Q \wedge R)$ to $(P \vee Q) \wedge (P \wedge R)$
  2. Convert conclusion to $(S \vee Q ) \wedge (P \vee Q)$
  3. Negate conclusion $\neg((S \vee Q ) \wedge (P \vee Q))$
  4. De Morgan's law to conclusion $\neg(S \vee Q) \vee \neg(P \vee Q)$
  5. De Morgan's Law again to conclusion $(\neg S \wedge \neg Q) \vee (\neg P \wedge \neg Q)$

After this I am lost what to do next. Can anyone help?


1 Answer 1


Yes, the conjunctive normal form for $P\vee(Q\wedge R)$ is $(P\vee Q)\wedge (P\vee R)$

The CNF for $S$ is of course, $S$.

And your work at finding the CNF for the negation of the conclusion is okay so far.†   Next distribute $(\neg S \wedge \neg Q) \vee (\neg P \wedge \neg Q)$ to obtain its CNF: $(\neg S\vee \neg P)\wedge\neg Q$.

So you just need to resolve $\{(P,Q),(P,R),S,(\neg S,\neg P),\neg Q\}$ to a contradiction.


† Though it would have been easier to just negate the DNF into a CNF using de Morgan's rule twice. $\neg((S\wedge P)\vee Q)=(\neg S\vee\neg P)\wedge\neg Q$ with no need to convert, negate, then convert again.


You must log in to answer this question.

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