Particularly important types of canonical normal forms are the conjunctive canonical normal form $\operatorname{ccnf}$ and the disjunctive canonical normal form $\operatorname{dcnf}$, which we will now formally define:
Let $\phi$ be a proposition with the Boolean variables $x_1,\ldots,x_n.$
A conjunctive canonical normal form of $\phi$ is a proposition $\operatorname{ccnf}(\phi)$ such that: * $\operatorname{ccnf}(\phi)$ is a canonical normal form of $\phi$, i.e. $\phi$ and $\operatorname{ccnf}(\phi)$ have identical Boolean functions $f_\phi=f_{\operatorname{ccnf}(\phi)}.$ * $\operatorname{ccnf}(\phi)$ has the following syntax: $$\begin{array}{rcl}\operatorname{ccnf}(\phi)&=&M_1\wedge \ldots \wedge M_n\\ &=&\bigwedge_{i=1}^n(\neg)x_1\vee \ldots\vee (\neg)x_n, \end{array}$$ where all maxterms $M_i$ are pairwise different.
A disjunctive canonical normal form of $\phi$ is a proposition $\operatorname{dcnf}(\phi)$ such that: * $\operatorname{dcnf}(\phi)$ is a canonical normal form of $\phi$, i.e. $\phi$ and $\operatorname{dcnf}(\phi)$ have identical Boolean functions $f_\phi=f_{\operatorname{dcnf}(\phi)}.$ * $\operatorname{dcnf}(\phi)$ has the following syntax: $$\begin{array}{rcl}\operatorname{dcnf}(\phi)&=&m_1\vee \ldots \vee m_n\\ &=&\bigvee_{i=1}^n(\neg)x_1\wedge \ldots\wedge (\neg)x_n, \end{array}$$ where all minterms $m_i$ are pairwise different.
Examples: 1
Lemmas: 2
Proofs: 3 4
