# Show that this formula is a tautology by converting to CNF

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?

• You should now use the distributive laws for AND and OR to massage both sides of the main connective into CNF. – A.Sh Aug 28 '16 at 12:00
• @A.Sh are there distributive laws for formulas involving four propositional letters? – PythonNewb Aug 28 '16 at 12:42

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

• Using this I got $P\ \land\ (\neg Q\ \lor\ R)\ \land\ (\neg S\ \lor\ \neg R\ \lor\ Q)\ \land\ (\neg S\ \lor\ \neg P)$, but I don't think this is correct, because this formula cannot show that the original is a tautology – PythonNewb Aug 28 '16 at 12:52
• Okay, I've fixed that issue, and now I got $P\ \land\ (\neg Q\ \lor\ R)\ \land\ (\neg S\ \lor\ \neg R)\ \land\ (\neg S\ \lor\ Q)\ \land\ (\neg S\ \lor\ P)$, which can still not prove that the original is a tautology – PythonNewb Aug 28 '16 at 13:10
• "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$." Can you please expand on this? It is very interesting – PythonNewb Aug 28 '16 at 13:50
• @PythonNewb: Do you still have some doubts, or is it ok now? – Gur Ismael Aug 28 '16 at 17:43
• I think understand now, but there is still no way to perform the resolution method on your CNF formula, which is throwing me off – PythonNewb Aug 29 '16 at 1:09