I'm working through some refutation proof questions for propositional logic, and I've come across the following question:
Show that the following formula is a tautology by negating it and then using refutation $$(P\ \land\ (Q\ \Rightarrow\ R))\ \Rightarrow\ ((S\ \lor\ P)\ \land\ (\neg R\ \Rightarrow\ \neg Q))$$
What I understand is I need to negate the entire formula and then convert it into CNF before performing the resolution/refutation proof. What I'm stuck on is the negation and convert to CNF part. Here's what I did:
Eliminate $\Rightarrow$:
$$(P\ \land\ (\neg Q \lor\ R))\ \Rightarrow\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$
$$\neg(P\ \land\ (\neg Q \lor\ R))\ \lor\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$
Now perform the negation step:
$$\neg(\neg(P\ \land\ (\neg Q \lor\ R))\ \lor\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q)))$$
Demorgans to push the negation into the formula:
$$\neg\neg(P\ \land\ (\neg Q \lor\ R))\ \land\ \neg((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$
$$(P\ \land\ (\neg Q \lor\ R))\ \land\ \neg((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$
$$(P\ \land\ (\neg Q \lor\ R))\ \land\ (\neg(S\ \lor\ P)\ \lor\ \neg(R\ \lor\ \neg Q))$$
$$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \land\ \neg P)\ \lor\ (\neg R\ \land\ Q))$$
And this is where I get stuck. I'm not sure how to proceed from here, because of that term on the right of the middle $\land$.
How do I proceed to convert this into CNF?
In these situations you need to you the distributivity laws, in your case you should proceed using
$$(a\wedge b)\vee c \leftrightarrow (a\vee c)\wedge (a\vee b), $$
where $$c:=(\neg R\wedge Q).$$
So the complete solution is as follows: $$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \land\ \neg P)\ \lor\ (\neg R\ \land\ Q))$$ $$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \vee\ \neg R)\ \wedge\ (\neg S\ \vee\ Q)\ \wedge (\neg P\ \vee \neg R)\ \wedge (\neg P\vee Q))$$
To satisfy this formula it must be the case $v(P)=1$, then we must have $v(R)=0$ and $v(Q)=1$, therefore this valuation cannot satisfy the clause $\neg Q \vee R$.
Resolution: You can (using resolution) infer $\{Q,\neg R\}$ applying $P$ to $\neg P\vee Q$ and $\neg P\vee\neg R$. Finally $\{Q,\neg R\}$ and $\neg Q\vee R$ gives the set $\{\neg R,R\}$, which implies the formula cannnot be satisfiable.
Comment: If you want to show that a formula is tautology, I would not negate the original formula, just transform it into conjunctive normal form. The formula is then a tautology if and only if every every clause of the CNF contains both $A$ and $\neg A$ for some atom $A$.
Proof of the last claim: from right to left: consider any valuation $v$ then it obviously must satisfy every clause, because it contains some $A$ and $\neg A$. On the other hand if you have some clause where for every atom $A$ at least on of $A$ and $\neg A$ is not in the clause. It is enough to define $v(A)=0$ iff $A$ is in the clause. It easily follows that vv does not satisfy the clause and hence the whole formula. QED