= Solution
First eliminate implication and biconditional using the <logical equivalences>
$$
A\to B\equiv\neg A\lor B,\qquad A\leftrightarrow B\equiv(\neg A\lor B)\land(\neg B\lor A).
$$
Push negations inwards using <De Morgan's laws> and eliminate double negations. <Structural induction> leaves only literals joined by conjunction and disjunction.
Now induct on that remaining expression. A literal is already in <conjunctive normal form>. A conjunction of two <conjunctive normal forms> is again one after associating its clauses. For a disjunction, write the two inductively obtained forms as $\bigwedge_i C_i$ and $\bigwedge_j D_j$ and use distributivity:
$$
\boxed{\left(\bigwedge_i C_i\right)\lor\left(\bigwedge_j D_j\right)\equiv\bigwedge_{i,j}(C_i\lor D_j).}
$$
Each $C_i\lor D_j$ is a clause. All operations preserve <logical equivalence>, proving the required form exists.
Back to article page
