# Show with resolution proof that expression is a tautology

I have the boolean expression:

$$((\neg A \lor B) \land (\neg B \lor \neg C))\implies (A\implies \neg C)$$

I have reshaped this so far that no equivalence and no implication is included. As far as I know, it is important for the resolution that the Boolean function is in CNF. My transformation then flows into this expression: $$((\neg A \lor B) \land (\neg B \lor \neg C))\implies (A\implies \neg C)$$ $$((\neg A \lor B) \land (\neg B \lor \neg C))\implies (\neg A \lor \neg C)$$ $$\neg((\neg A \lor B) \land (\neg B \lor \neg C))\lor (\neg A \lor \neg C)$$ $$(\neg(\neg A \lor B) \lor \neg(\neg B \lor \neg C))\lor (\neg A \lor \neg C)$$ $$((A \land \neg B) \lor (B \land C))\lor (\neg A \lor \neg C)$$ That is not yet CNF form, right? My question is therefore, can someone go to me the transformation steps? How to get to the CNF form?

If I had the CNF form, I could show a tautology with the resolution. For this I need the clause set from the CNF.

To get into CNF, distribute any $\lor$'s over $\land$'s. So:

$$((A \land \neg B) \lor (B \land C))\lor (\neg A \lor \neg C) \Leftrightarrow$$

$$(((A \land \neg B) \lor B) \land (A \land \neg B) \lor C))) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$((A \lor B) \land (\neg B \lor B) \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$((A \lor B) \land \top \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$((A \lor B) \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$((A \lor B) \lor (\neg A \lor \neg C)) \land ((A \lor C) \lor (\neg A \lor \neg C)) \land ((\neg B \lor C) \lor (\neg A \lor \neg C)) \Leftrightarrow$$

$$(A \lor B \lor \neg A \lor \neg C) \land (A \lor C \lor \neg A \lor \neg C) \land (\neg B \lor C \lor \neg A \lor \neg C) \Leftrightarrow$$

$$\top \land \top \land \top \Leftrightarrow$$

$$\top$$

Hmmm....

OK, so we have taken the statement as is and proven it to be a tautology!

... but not through resolution ...

In fact, you got the wrong set-up! To prove this statement to be a tautology through resolution, you need to first negate the statement, and then put it into CNF, thus into clauses, and then derive the empty clause through resolution:

$$\neg (((\neg A \lor B) \land (\neg B \lor \neg C))\to (A\to \neg C)) \Leftrightarrow$$

$$((\neg A \lor B) \land (\neg B \lor \neg C))\land \neg (A \to \neg C) \Leftrightarrow$$

$$(\neg A \lor B) \land (\neg B \lor \neg C)\land A \land C$$

This is now in CNF! ... and you will find resolution is now trivial

• Hi and thank you for your good answer! So if I understand that correctly, I must first negate the first expression and then reshape it into CNF correctly. So: $\ neg (((\ neg A \ lor B) \ land (\ neg B \ lor \ neg C)) \ implies (A \ implies \ neg C))$ Commented Jun 18, 2018 at 14:06
• @JohnSchulz Yes! Just added that to the answer ... and sorry, I can't bring myself to use $\Rightarrow$ for the conditional; I much prefer to use $\rightarrow$ Commented Jun 18, 2018 at 14:09
• Thanks again for your help! I'm just trying to understand your transformation exactly. Commented Jun 18, 2018 at 14:13
• @JohnSchulz Sorry if that went a bit fast ... I used the equivalence $\neg (P \to Q) \Leftrightarrow P \land \neg Q$. But you can always derive that: $\neg (P \to Q) \Leftrightarrow \neg (\neg P \lor Q) \Leftrightarrow \neg \neg P \land \neg Q \Leftrightarrow P \land \neg Q$. ... oh, and I had a negation that shouldn't have been there ... fixed! Commented Jun 18, 2018 at 14:14
• Ah ok, now it's true for me too. I've been thinking all the time about recalculating your solution that I made a mistake. But nice that you have corrected the error yet! Now I understand the solution completely! Thank you very much! Commented Jun 18, 2018 at 14:20

To prove $(X\wedge Y)\to Z$ is a tautology, by resolution, you seek to prove $(X\wedge Y\wedge\neg Z)$ is a contradiction (ie false).   After all, if the junction of $X$ and $Y$ does imply $Z$ then it shall contradict $\neg Z$.

So, since the negation of $A\to\neg C$ is $A\wedge\neg\neg C$, therefore to prove $((\neg A\vee B)\wedge(\neg B\vee\neg C))\to(A\to\neg C)$, you must simply show that $((\neg A\vee B)\wedge(\neg B\vee\neg C))\wedge(A\wedge\neg\neg C)$ is a contradiction.

That is, that the clausal form $\{(\neg A, B),(\neg B,\neg C),(A),(\neg\neg C)\}$ may be resolved to an empty set.

• Hi, why is your clausal form not: M = {{\ neg a, b}, {\ neg b, \ neg c}, {a}, {c}}? I have a logic book in which this topic is unfortunately poorly explained. But there is something like this as an example: a = (p \ lor q \ lor \ neg r) \ land (\ neg p) ... Which results in the following clause amount: M = {{p, q, \ negr}, {\ neg p}, ...} Commented Jun 18, 2018 at 14:30
• Because of a typo. Commented Jun 18, 2018 at 14:31
• Ok, that explanins my question. Thank you, too. Then you can ignore my objection above :) Commented Jun 18, 2018 at 14:34