# Converting a propositional logic formula to Clause Normal Form

Given the following propositional logic formula: $$((A\implies B)\land (A\implies (B\implies C)))\implies (A\implies C)$$ I would like to convert it to Clause Normal Form. Here's what I did: $$\neg ((\neg A\lor B)\land (\neg A\lor (\neg B\lor C)))\lor (\neg A\lor C)$$ $$\neg ((\neg A\lor B)\land (\neg A\lor \neg B\lor C))\lor (\neg A\lor C)$$

I know that it's not the final step to obtain the CNF, but I can see that there is a similarity with the (given) solutions $$\{\neg A, B \}, \{\neg A, \neg B, C\}, \{A\}, \{\neg C\}$$.

How can I get to the final CNF form?

You did nothing wrong in converting:

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

to:

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

However, this latter statement will not give you the indicated Answer.

Here is what I am pretty sure is going on:

You are supposed to prove that the given statement is a tautology by using some method that requires you to use CNF, such as resolution, or Davis-Putnam. However, all those methods work like a proof by contradiction: You first have to negate the statement to be proven, then put that into CNF, and then apply your method to derive the empty clause (which is a contradiction)

So, you need to take the negation of what you got:

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

which gives you:

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

and thus:

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

• Thank you very much for your answer! This is exactly what I was looking for :) Commented Dec 24, 2019 at 17:15
• @Kevin You're welcome! :) Commented Dec 24, 2019 at 17:36

By De Morgan's law: $$A\lor B = \neg (\neg A \wedge \neg B)$$. Applying it to the second to last disjunction yields:

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

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

Applying the same law to the last disjunction yields:

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

Which is the CNF.

• Thank you! :) :) Commented Dec 24, 2019 at 17:15