How to prove this using resolution theorem or resolution refutation?

2017-12-03 03:06:59

I need to prove P v (Q ^ R), S : (S ^ P) v Q using resolution theorem or resolution refutation. This is my proof:

Convert P v (Q ^ R) to (P v Q) ^ (P ^ R)

Convert conclusion to (S v Q ) ^ (P v Q)

Negate conclusion ¬((S v Q ) ^ (P v Q))

De Morgan's law to conclusion ¬(S v Q) v ¬(P v Q)

De Morgan's Law again to conclusion (¬S ^ ¬Q) v (¬P ^ ¬Q)

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

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\ne

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

    2017-12-03 05:47:52