Converting logic formula to CNF
$$\big( (A \lor B) \land ((B \leftrightarrow A) \to C) \big) \lor (C \to \neg A)$$
I have attached an image showing my workout. Is this correct?blue [enter image description here][1]
I can use the following equivalences:
x∧(y∧z) = (x∧y)∧z, x∧y=y∧x, x∧x=x x∨(y∨ z)=(x∨y)∨z, x∨y=y∨x, x∨x=x x∧(y∨z)=(x∧y)∨(x∧z), x∨(y∧z) = (x∨y)∧(x∨z) x→y = (¬x)∨y x↔y=(x∧y)∨(¬x;∨¬y) ¬¬x=x ¬(x∧y)=(¬x)∨(¬y), ¬(x∨y)=(¬x)∧(¬y)
In your last step ("cancel double negation"), you don't really have a double negation yet. You take $\neg (\neg B \vee A)$ and resolve it as $\neg \neg B \vee \neg A = B \vee \neg A$; you have thus implicitly distributed the negation over the disjunction, which you cannot do. Instead, you need to apply de Morgan's law again to get $\neg \neg B \land \neg A = B \land \neg A$.
You make the same mistake in the way you resolve $\neg(\neg A \lor B)$; this should again resolve by de Morgan's law to $\neg \neg A \land \neg B = A \land \neg B$.
Once you fix these, you can continue the process of working the expression into CNF.