3
$\begingroup$

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?

1 Answers 1

1

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.