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.


2 Answers 2


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$$



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

  • $\begingroup$ 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)) $ $\endgroup$ Commented Jun 18, 2018 at 14:06
  • $\begingroup$ @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$ $\endgroup$
    – Bram28
    Commented Jun 18, 2018 at 14:09
  • $\begingroup$ Thanks again for your help! I'm just trying to understand your transformation exactly. $\endgroup$ Commented Jun 18, 2018 at 14:13
  • $\begingroup$ @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! $\endgroup$
    – Bram28
    Commented Jun 18, 2018 at 14:14
  • $\begingroup$ 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! $\endgroup$ 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.

  • $\begingroup$ 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}, ...} $\endgroup$ Commented Jun 18, 2018 at 14:30
  • $\begingroup$ Because of a typo. $\endgroup$ Commented Jun 18, 2018 at 14:31
  • $\begingroup$ Ok, that explanins my question. Thank you, too. Then you can ignore my objection above :) $\endgroup$ Commented Jun 18, 2018 at 14:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .