# How to prove correctness of CNF transformation?

Let $f$ be a propositional formula in negative normal form. It holds:

Applying the rules $$A\lor(B\land C)\to(A\lor V)\land(A\lor C)$$ and $$(B\land C)\lor A\to(B\lor A)\land(C\lor A)$$ as many as possible leads to a CNF formula of $f$.

How can one prove the statement above?

My approach: Induction over the structure of formula $f$. The cases with $f=x_i$, $f = \neg x_i$ and $f = f_1 \land f_2$ are easy.

But I have trouble with the last case $f = f_1 \lor f_2$. With the induction hypothesis one can say that applying the rules of $f_1$ and $f_2$ leads to formulas in CNF for both subformulas. But where to go from here?

-

HINT: Suppose that $f_1=s_1\land s_2\land\ldots\land s_m$ for some clauses $s_1,\dots,s_m$ that are disjunctions of one-literal clauses (i.e., clauses of the form $A$ or $\neg A$). If $t$ is a one-literal clause, then

\begin{align*} f_1\lor t&=(s_1\land s_2\land\ldots\land s_m)\lor t\\ &\equiv\Big((s_1\land\ldots\land s_{m-1})\land s_m\Big)\lor t\\ &\to\Big((s_1\land\ldots\land s_{m-1})\lor t\Big)\land(s_m\lor t)\;; \end{align*}

you can use this idea to show by induction on $m$ that $f_1\lor t$ reduces to $\bigwedge_{k=1}^m(s_m\lor t)$, which is in CNF.

Now let $f_2=t_1\land t_2\land\ldots\land t_n$ for some clauses $t_1,\dots,t_n$ that are disjunctions of one-literal clauses. Show by a similar induction on $n$ that

$$f_1\lor f_2\overset{*}\longrightarrow\bigwedge_{i=1}^n\bigwedge_{k=1}^m(s_m\lor t_i)\;,$$

where $\overset{*}\longrightarrow$ means that the righthand side can be obtained from the lefthand side by a sequence of allowable reductions.

-
Thank you, that helped a lot. –  John Threepwood Jan 29 '13 at 14:38