# 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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9390482306480408, "perplexity": 191.25782919449563}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 20, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-47/segments/1573496670559.66/warc/CC-MAIN-20191120134617-20191120162617-00124.warc.gz"}