View source for Conjunctive normal form

{{TEX|done}}{{MSC|03B05}}

A propositional formula of the form
\begin{equation}\label{eq1}
  \bigwedge_{i=1}^n \bigvee_{j=1}^{m_i} \, C_{ij}
\end{equation}
where each $C_{ij}$, $i=1,\ldots,n$; $j = 1,\ldots,m_i$, is either an atomic formula (a variable or constant) or the negation of an atomic formula. The conjunctive normal form \ref{eq1} is a [[tautology]] if and only if for every $i$ one can find both formulas $p$ and $\neg p$ among the $C_{i1},\ldots,C_{im_i}$, for some atomic formula $p$. Given any propositional formula $A$, one can construct a conjunctive normal form $B$ equivalent to it and containing the same variables and constants as $A$. This $B$ is called the conjunctive normal form of $A$.



====Comments====
The dual of a conjunctive normal form is a [[disjunctive normal form]]. Both are also used in the theory of Boolean functions (cf. [[Boolean functions, normal forms of|Boolean functions, normal forms of]]).