Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 1 down vote accepted

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.

share|cite|improve this answer
Thank you, that helped a lot. – John Threepwood Jan 29 '13 at 14:38

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.