Converting a propositional logic formula to Clause Normal Form

Question

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?

Answer 1

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

Answer 2

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.