Editing Conjunctive normal form

{{Short description|Standard form of Boolean function}}
{{distinguish|Chomsky normal form}}

In [[Boolean algebra]], a [[Formula (mathematical logic)|formula]] is in '''conjunctive normal form''' ('''CNF''') or '''clausal normal form''' if it is a [[logical conjunction|conjunction]] of one or more [[clause (logic)|clauses]], where a clause is a [[logical disjunction|disjunction]] of [[literal (mathematical logic)|literal]]s; otherwise put, it is a '''product of sums''' or '''an AND of ORs'''.

In automated theorem proving, the notion "''clausal normal form''" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.

==Definition==
A logical formula is considered to be in CNF if it is a [[logical conjunction|conjunction]] of one or more [[logical disjunction|disjunctions]] of one or more [[literal (mathematical logic)|literals]]. As in [[disjunctive normal form]] (DNF), the only propositional operators in CNF are [[logical disjunction|or]] (<math>\vee</math>), [[logical conjunction|and]] (<math>\and</math>), and [[negation|not]] (<math>\neg</math>). The ''not'' operator can only be used as part of a literal, which means that it can only precede a [[propositional variable]].

The following is a [[context-free grammar]] for CNF:
: ''CNF'' <math>\, \to \,</math> ''Disjunct'' <math>\, \mid \, </math> ''Disjunct'' <math>\, \land \,</math> ''CNF''
: ''Disjunct'' <math>\, \to \,</math> ''Literal'' <math>\, \mid\, </math> ''Literal'' <math>\, \lor \,</math> ''Disjunct''
: ''Literal'' <math>\, \to \,</math> ''Variable'' <math>\, \mid \,</math> <math>\, \neg \,</math> ''Variable''
Where ''Variable'' is any variable.

All of the following formulas in the variables <math>A,B,C,D,E,</math> and <math>F</math> are in conjunctive normal form:

* <math>(A \lor \neg B \lor \neg C) \land (\neg D \lor E \lor F \lor D \lor F)</math>
* <math>(A \lor B) \land (C)</math>
* <math>(A \lor B)</math>
* <math>(A)</math>

The following formulas are '''not''' in conjunctive normal form:
* <math>\neg (A \land B)</math>, since an AND is nested within a NOT
*<math>\neg(A \lor B) \land C</math>, since an OR is nested within a NOT
* <math>A \land (B \lor (D \land E))</math>, since an AND is nested within an OR

==Conversion to CNF==
In [[classical logic]] each [[propositional formula]] can be converted to an [[logical equivalence|equivalent]] formula that is in CNF.{{sfn|Howson|2005|page=46}} This transformation is based on rules about [[logical equivalence]]s: [[double negation elimination]], [[De Morgan's laws]], and the [[distributive law]].

=== Basic algorithm ===
The algorithm to compute a CNF-equivalent of a given propositional formula <math>\phi</math> builds upon <math>\lnot \phi</math> in [[Disjunctive normal form|disjunctive normal form (DNF)]]: step 1.<ref name="dnf" /><br/>
Then <math>\lnot \phi_{DNF}</math> is converted to <math>\phi_{CNF}</math> by swapping ANDs with ORs and vice versa while negating all the literals. Remove all <math>\lnot \lnot</math>.{{sfn|Howson|2005|page=46}}

==== Conversion by syntactic means ====
Convert to CNF the propositional formula <math>\phi</math>.

'''Step 1''': Convert its negation to disjunctive normal form.<ref name="dnf">see {{slink|Disjunctive normal form#Conversion to DNF}}</ref> 

<math>\lnot \phi_{DNF} = (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m)</math>,{{refn|<math>1 \le m \le</math> [[Disjunctive normal form#max_conjunctions|maximum number of conjunctions]] for <math>\phi</math>}}

where each <math>C_i</math> is a conjunction of literals <math>l_{i1} \land l_{i2} \land \ldots \land l_{in_i}</math>.{{refn|<math>1 \le in_i \le</math> [[Disjunctive normal form#max conjunctions|maximum number of literals]] for <math>\phi</math>}}

'''Step 2''': Negate <math>\lnot \phi_{DNF}</math>.
Then shift <math>\lnot</math> inwards by applying the [[De Morgan's laws#Formal notation|(generalized) De Morgan's equivalences]] until no longer possible.
<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot (C_1 \lor C_2 \lor \ldots \lor C_i \lor \ldots \lor C_m) \\
&\leftrightarrow \lnot C_1 \land \lnot C_2 \land \ldots \land \lnot C_i \land \ldots \land \lnot C_m &&\text{// (generalized) D.M.} 
\end{align}</math>
where<math display="block">\begin{align}
\lnot C_i &= \lnot (l_{i1} \land l_{i2} \land \ldots \land l_{in_i}) \\
&\leftrightarrow (\lnot l_{i1} \lor \lnot l_{i2} \lor \ldots \lor \lnot l_{in_i}) &&\text{// (generalized) D.M.}
\end{align}</math>

'''Step 3''': Remove all double negations.

'''Example'''

Convert to CNF the propositional formula
<math>\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.{{refn|name=phiverbose|1=<math>\phi</math> = (('''[[Negation|NOT]]''' (p '''[[Logical conjunction|AND]]''' q)) '''[[If and only if|IFF]]''' (('''[[Negation|NOT]]''' r) '''[[Sheffer stroke|NAND]]''' (p '''[[XOR]]''' q)))}}

The (full) DNF equivalent of its negation is<ref name="dnf" /><br/>
<math> \lnot \phi_{DNF} =
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) </math>

<math display="block">\begin{align}
\phi &\leftrightarrow \lnot \lnot \phi_{DNF} \\
&= \lnot \{
(      p \land       q \land       r) \lor
(      p \land       q \land \lnot r) \lor
(      p \land \lnot q \land \lnot r) \lor
(\lnot p \land       q \land \lnot r) \} \\
&\leftrightarrow
\underline{\lnot( p \land       q \land       r)} \land
\underline{\lnot( p \land       q \land \lnot r)} \land
\underline{\lnot( p \land \lnot q \land \lnot r)} \land
\underline{\lnot(\lnot p  \land q \land \lnot r)} &&\text{// generalized D.M. } \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor \lnot \lnot r) \land
(\lnot p \lor \lnot \lnot q \lor \lnot \lnot r) \land
(\lnot \lnot p \lor \lnot q \lor \lnot \lnot r) &&\text{// generalized D.M. } (4 \times) \\
&\leftrightarrow
(\lnot p \lor  \lnot q \lor \lnot r) \land
(\lnot p \lor  \lnot q \lor       r) \land
(\lnot p \lor        q \lor       r) \land
(      p \lor \lnot q \lor        r) &&\text{// remove all } \lnot \lnot \\
&= \phi_{CNF}
\end{align}</math>

==== Conversion by semantic means ====
A CNF equivalent of a formula can be derived from its [[truth table]]. Again, consider the formula
<math display="block">\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.{{refn|name=phiverbose}}

The corresponding [[truth table]] is
{| class="wikitable" style="text-align:center; padding-left: 1.5em;"
! <math>p</math>
! <math>q</math>
! <math>r</math>
! style="background:black"| 
! <math>(</math>
! <math>\lnot</math>
! <math>(p \land q)</math>
! <math>)</math>
! <math>\leftrightarrow</math>
! <math>(</math>
! <math>\lnot r</math>
! <math>\uparrow</math>
! <math>(p \oplus q)</math>
! <math>)</math>
|-
| style="background:lightgreen"|T || style="background:lightgreen"|T || style="background:lightgreen"|T ||style="background:black"| || || F || T || || style="background:papayawhip" | '''F''' || || F || T || F ||
|-
| style="background:lightgreen"|T || style="background:lightgreen"|T || style="background:lightgreen"|F ||style="background:black"| || || F || T || || style="background:papayawhip" | '''F''' || || T || T || F ||
|-
| T || F || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || T ||
|-
| style="background:lightgreen"|T || style="background:lightgreen"|F || style="background:lightgreen"|F ||style="background:black"| || || T || F || || style="background:papayawhip" | '''F''' || || T || F || T ||
|-
| F || T || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || T ||
|-
| style="background:lightgreen"|F || style="background:lightgreen"|T || style="background:lightgreen"|F ||style="background:black"| || || T || F || || style="background:papayawhip" | '''F''' || || T || F || T ||
|-
| F || F || T ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || F || T || F ||
|-
| F || F || F ||style="background:black"| || || T || F || || style="background:papayawhip" | T || || T || T || F ||
|}

A CNF equivalent of <math>\phi</math> is
<math display="block">
(\lnot p \lor \lnot q \lor \lnot r) \land
(\lnot p \lor \lnot q \lor       r) \land
(\lnot p \lor       q \lor       r) \land
(      p \lor \lnot q \lor       r)
</math>

Each disjunction reflects an assignment of variables for which <math>\phi</math> evaluates to F(alse).<br/>
If in such an assignment a variable <math>V</math>
* is T(rue), then the literal is set to <math>\lnot V</math> in the disjunction,
* is F(alse), then the literal is set to <math>V</math> in the disjunction.

===Other approaches===
Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF. However, in some cases this conversion to CNF can lead to an exponential explosion of the formula. For example, translating the non-CNF formula

<math display="block">(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \ldots \vee (X_n \wedge Y_n)</math> 

into CNF produces a formula with <math>2^n</math> clauses:

<math display="block">(X_1 \vee X_2 \vee \ldots \vee X_n) \wedge (Y_1 \vee X_2 \vee \ldots \vee X_n) \wedge (X_1 \vee Y_2 \vee \ldots \vee X_n) \wedge (Y_1 \vee Y_2 \vee \ldots \vee X_n) \wedge \ldots \wedge (Y_1 \vee Y_2 \vee \ldots \vee Y_n).</math>

Each clause contains either <math>X_i</math> or <math>Y_i</math> for each <math>i</math>.

There exist transformations into CNF that avoid an exponential increase in size by preserving [[Boolean satisfiability problem|satisfiability]] rather than [[logical equivalence|equivalence]].{{sfn|Tseitin |1968}}{{sfn|Jackson|Sheridan|2004}} These transformations are guaranteed to only linearly increase the size of the formula, but introduce new variables. For example, the above formula can be transformed into CNF by adding variables <math>Z_1,\ldots,Z_n</math> as follows:

<math display="block">(Z_1 \vee \ldots \vee Z_n) \wedge
(\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge
\ldots \wedge 
(\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n). </math>

An [[interpretation (logic)|interpretation]] satisfies this formula only if at least one of the new variables is true. If this variable is <math>Z_i</math>, then both <math>X_i</math> and <math>Y_i</math> are true as well. This means that every [[Model theory|model]] that satisfies this formula also satisfies the original one. On the other hand, only some of the models of the original formula satisfy this one: since the <math>Z_i</math> are not mentioned in the original formula, their values are irrelevant to satisfaction of it, which is not the case in the last formula. This means that the original formula and the result of the translation are [[Equisatisfiability|equisatisfiable]] but not [[logical equivalence|equivalent]].

An alternative translation, the [[Tseitin transformation]], includes also the clauses <math>Z_i \vee \neg X_i \vee \neg Y_i</math>. With these clauses, the formula implies <math>Z_i \equiv X_i \wedge Y_i</math>; this formula is often regarded to "define" <math>Z_i</math> to be a name for <math>X_i \wedge Y_i</math>.

== Maximum number of disjunctions ==
<span id="max_disjunctions"></span>
Consider a propositional formula with <math>n</math> variables, <math>n \ge 1</math>.

There are <math>2n</math> possible literals: <math>L = \{ p_1, \lnot p_1, p_2, \lnot p_2, \ldots, p_n, \lnot p_n\}</math>.

<math>L</math> has <math>(2^{2n} -1)</math> non-empty subsets.{{refn|<math>\left|\mathcal{P}(L)\right| = 2^{2n}</math>}}

This is the maximum number of disjunctions a CNF can have.{{refn|name=noreps|It is assumed that repetitions and variations (like <math>(a \land b) \lor (b \land a) \lor (a \land b \land b)</math>) based on the [[Commutative property|commutativity]] and [[Associative property|associativity]] of <math>\lor</math> and <math>\land</math> do not occur.}}

All truth-functional combinations can be expressed with <math>2^{n}</math> disjunctions, one for each row of the truth table.<br/>In the example below they are underlined.

'''Example'''

Consider a formula with two variables <math>p</math> and <math>q</math>.

The longest possible CNF has <math>2^{(2 \times 2)} -1 = 15</math> disjunctions:{{refn|name=noreps}}
<math display="block"> 
\begin{array}{lcl}
(\lnot p) \land (p) \land (\lnot q) \land (q) \land \\
(\lnot p \or       p) \land
\underline{(\lnot p \or \lnot q)} \land
\underline{(\lnot p \or       q)} \land
\underline{(      p \or \lnot q)} \land
\underline{(      p \or       q)} \land
(\lnot q \or       q) \land \\
(\lnot p \or       p \or \lnot q) \land	
(\lnot p \or       p \or       q) \land	
(\lnot p \or \lnot q \or       q) \land	
(      p \or \lnot q \or       q) \land \\
(\lnot p \or       p \or \lnot q \or q)
\end{array}</math>

This formula is a [[contradiction]]. It can be simplified to <math>(\neg p \land p)</math> or to <math>(\neg q \land q)</math>, which are also contradictions, as well as valid CNFs.

==Computational complexity==
An important set of problems in [[computational complexity theory|computational complexity]] involves finding assignments to the variables of a Boolean formula expressed in conjunctive normal form, such that the formula is true. The ''k''-SAT problem is the problem of finding a satisfying assignment to a Boolean formula expressed in CNF in which each disjunction contains at most ''k'' variables. [[Boolean satisfiability problem|3-SAT]] is [[NP-complete]] (like any other ''k''-SAT problem with ''k''>2) while [[2-satisfiability|2-SAT]] is known to have solutions in [[polynomial time]]. As a consequence,{{refn|since one way to check a CNF for satisfiability is to convert it into a [[Disjunctive normal form|DNF]], the satisfiability of which can be checked in [[Time complexity#Linear time|linear time]]}} the task of converting a formula into a [[Disjunctive normal form|DNF]], preserving satisfiability, is [[NP-hard]]; [[Boolean algebra#Duality principle|dually]], converting into CNF, preserving [[Satisfiability and validity|validity]], is also NP-hard; hence equivalence-preserving conversion into DNF or CNF is again NP-hard.

Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts.

A formula in CNF can be converted into an equisatisfiable formula in "''k''CNF" (for ''k''&ge;3) by replacing each conjunct with more than ''k'' variables <math>X_1 \vee \ldots \vee X_k \vee \ldots \vee X_n</math> by two conjuncts <math>X_1 \vee \ldots \vee X_{k-1} \vee Z</math> and <math>\neg Z \vee X_k \lor \ldots \vee X_n</math> with {{mvar|Z}} a new variable, and repeating as often as necessary.

==First-order logic==
In first order logic, conjunctive normal form can be taken further to yield the clausal normal form of a logical formula, which can be then used to perform [[Resolution (logic)#Resolution in first-order logic|first-order resolution]].
In resolution-based automated theorem-proving, a CNF formula 
{| 
|-
||
|| <math>(</math>
|| <math>l_{11}</math>
|| <math>\lor</math>
|| <math>\ldots</math>
|| <math>\lor</math>
|| <math>l_{1n_1}</math>
|| <math>)</math>
|| <math>\land</math>
|| <math>\ldots</math>
|| <math>\land</math>
|| <math>(</math>
|| <math>l_{m1}</math>
|| <math>\lor</math>
|| <math>\ldots</math>
|| <math>\lor</math>
|| <math>l_{mn_m}</math>
|| <math>)</math>
||
|| ,{{refn|<math>1 \le m \le</math> [[Conjunctive normal form#max disjunctions|maximum number of disjunctions]]<br/><math>1 \le in_i \le</math> [[Conjunctive normal form#max disjunctions|maximum number of literals]]}} is commonly represented as a set of sets
|-
|| <math>\{</math>
|| <math>\{</math>
|| <math>l_{11}</math>
|| <math>,</math>
|| <math>\ldots</math>
|| <math>,</math>
|| <math>l_{1n_1}</math>
|| <math>\}</math>
|| <math>,</math>
|| <math>\ldots</math>
|| <math>,</math>
|| <math>\{</math>
|| <math>l_{m1}</math>
|| <math>,</math>
|| <math>\ldots</math>
|| <math>,</math>
|| <math>l_{mn_m}</math>
|| <math>\}</math>
|| <math>\}</math>
|| .
|}
See below for an example.

===Converting from first-order logic===
To convert [[first-order logic]] to CNF:{{sfn|Russel|Norvig|2010|pages=345-347|loc=9.5.1 Conjunctive normal form for first-order logic}}
#Convert to [[negation normal form]].
## Eliminate implications and equivalences: repeatedly replace <math>P \rightarrow Q</math> with <math>\lnot P \lor Q</math>; replace <math>P \leftrightarrow Q</math> with <math>(P \lor \lnot Q) \land (\lnot P \lor Q)</math>. Eventually, this will eliminate all occurrences of <math>\rightarrow</math> and <math>\leftrightarrow</math>.
##Move NOTs inwards by repeatedly applying [[De Morgan's Law|De Morgan's law]]. Specifically, replace <math>\lnot (P \lor Q)</math> with <math>(\lnot P) \land (\lnot Q)</math>; replace <math>\lnot (P \land Q)</math> with <math>(\lnot P) \lor (\lnot Q)</math>; and replace <math>\lnot\lnot P</math> with <math>P</math>; replace <math>\lnot (\forall x P(x))</math> with <math>\exists x \lnot P(x)</math>; <math>\lnot (\exists x P(x))</math> with <math>\forall x \lnot P(x)</math>. After that, a <math>\lnot</math> may occur only immediately before a predicate symbol.
#Standardize variables
##For sentences like <math>(\forall x P(x)) \lor (\exists x Q(x))</math> which use the same variable name twice, change the name of one of the variables. This avoids confusion later when dropping quantifiers. For example, <math>\forall x [\exists y \mathrm{Animal}(y) \land \lnot \mathrm{Loves}(x, y)] \lor [\exists y \mathrm{Loves}(y, x)]</math> is renamed to <math>\forall x [\exists y \mathrm{Animal}(y) \land \lnot \mathrm{Loves}(x, y)] \lor [\exists z \mathrm{Loves}(z,x)]</math>.
#[[Skolem normal form|Skolemize]] the statement
##Move quantifiers outwards: repeatedly replace <math>P \land (\forall x Q(x))</math> with <math>\forall x (P \land Q(x))</math>; replace <math>P \lor (\forall x Q(x))</math> with <math>\forall x (P \lor Q(x))</math>; replace <math>P \land (\exists x Q(x))</math> with <math>\exists x (P \land Q(x))</math>; replace <math>P \lor (\exists x Q(x))</math> with <math>\exists x (P \lor Q(x))</math>. These replacements preserve equivalence, since the previous variable standardization step ensured that <math>x</math> doesn't occur in <math>P</math>. After these replacements, a quantifier may occur only in the initial prefix of the formula, but never inside a <math>\lnot</math>, <math>\land</math>, or <math>\lor</math>. 
##Repeatedly replace <math>\forall x_1 \ldots \forall x_n \; \exists y \; P(y)</math> with <math>\forall x_1 \ldots \forall x_n \; P(f(x_1,\ldots,x_n))</math>, where <math>f</math> is a new <math>n</math>-ary function symbol, a so-called "[[Skolem normal form|Skolem function]]". This is the only step that preserves only satisfiability rather than equivalence. It eliminates all existential quantifiers.
#Drop all universal quantifiers.
#Distribute ORs inwards over ANDs: repeatedly replace <math>P \lor (Q \land R)</math> with <math>(P \lor Q) \land (P \lor R)</math>.

'''Example'''

As an example, the formula saying ''"Anyone who loves all animals, is in turn loved by someone"'' is converted into CNF (and subsequently into [[clause (logic)|clause]] form in the last line) as follows (highlighting replacement rule [[redex]]es in <math>{\color{red}{\text{red}}}</math>):

{|
|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>\forall y</math>
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\color{red}\rightarrow</math>
||
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\rightarrow</math>
||<math>(</math>
||<math>\exists</math>
||<math>y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||

|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>\forall y</math>
||
||
||
||<math>\lnot</math>
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\lor</math>
||
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\color{red}\rightarrow</math>
||<math>(</math>
||<math>\exists</math>
||<math>y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 1.1

|-
||<math>\forall x</math>
||<math>\color{red}\lnot</math>
||
||
||<math>(</math>
||<math>{\color{red}{\forall y}}</math>
||
||
||
||<math>\lnot</math>
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\lor</math>
||
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\lor</math>
||<math>(</math>
||<math>\exists</math>
||<math>y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 1.1

|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>\exists y</math>
||<math>\color{red}\lnot</math>
||<math>(</math>
||
||<math>\lnot</math>
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\color{red}\lor</math>
||
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||<math>)</math>
||<math>)</math>
||<math>\lor</math>
||<math>(</math>
||<math>\exists</math>
||<math>y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 1.2

|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>\exists y</math>
||
||
||<math>\color{red}\lnot</math>
||<math>\color{red}\lnot</math>
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\lor</math>
||<math>(</math>
||<math>\exists</math>
||<math>y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 1.2

|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>{\color{red}{\exists y}}</math>
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\lor</math>
||<math>(</math>
||<math>\color{red}\exists</math>
||<math>\color{red}y</math>
||<math>\mathrm{Loves}(</math>
||<math>y</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 1.2

|-
||<math>\forall x</math>
||
||
||
||<math>(</math>
||<math>\exists y</math>
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\color{red}\lor</math>
||<math>(</math>
||<math>\color{red}\exists</math>
||<math>\color{red}z</math>
||<math>\mathrm{Loves}(</math>
||<math>z</math>
||<math>,x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||
||by 2

|-
||<math>\forall x</math>
||<math>\exists z</math>
||
||
||<math>(</math>
||<math>{\color{red}{\exists y}}</math>
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||
||<math>)</math>
||<math>\color{red}\lor</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>z</math>
||<math>,x)</math>
||
||
||
||
||
||
||
||
||
||by 3.1

|-
||<math>\forall x</math>
||<math>{\color{red}{\exists z}}</math>
||
||
||
||<math>\exists y</math>
||
||<math>(</math>
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||<math>)</math>
||
||<math>\lor</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>z</math>
||<math>,x)</math>
||
||
||
||
||
||
||
||
||
||by 3.1

|-
||<math>\forall x</math>
||
||
||
||
||<math>{\color{red}{\exists y}}</math>
||
||<math>(</math>
||
||
||<math>\mathrm{Animal}(</math>
||<math>y</math>
||<math>)</math>
||<math>\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>y</math>
||<math>)</math>
||<math>)</math>
||
||<math>\lor</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>g(x)</math>
||<math>,x)</math>
||
||
||
||
||
||
||
||
||
||by 3.2

|-
||
||
||
||
||
||
||
||<math>(</math>
||
||
||<math>\mathrm{Animal}(</math>
||<math>f(x)</math>
||<math>)</math>
||<math>\color{red}\land</math>
||<math>\lnot</math>
||<math>\mathrm{Loves}(x,</math>
||<math>f(x)</math>
||<math>)</math>
||<math>)</math>
||
||<math>\color{red}\lor</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>g(x)</math>
||<math>,x)</math>
||
||
||
||
||
||
||
||
||
||by 4

|-
||
||
||
||<math>(</math>
||
||
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>f(x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||<math>\color{red}\lor</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>g(x)</math>
||<math>,x)</math>
||
||<math>)</math>
||<math>\color{red}\land</math>
||<math>(</math>
||<math>\lnot \mathrm{Loves}(x,f(x))</math>
||<math>\color{red}\lor</math>
||<math>\mathrm{Loves}(g(x),x)</math>
||<math>)</math>
||
||by 5

|-
||
||
||<math>\{</math>
||<math>\{</math>
||
||
||
||
||
||
||<math>\mathrm{Animal}(</math>
||<math>f(x)</math>
||<math>)</math>
||
||
||
||
||
||
||
||<math>,</math>
||
||
||
||<math>\mathrm{Loves}(</math>
||<math>g(x)</math>
||<math>,x)</math>
||
||<math>\}</math>
||<math>,</math>
||<math>\{</math>
||<math>\lnot \mathrm{Loves}(x,f(x))</math>
||<math>,</math>
||<math>\mathrm{Loves}(g(x),x)</math>
||<math>\}</math>
||<math>\}</math>
||([[clause (logic)|clause]] representation)

|}

Informally, the Skolem function <math>g(x)</math> can be thought of as yielding the person by whom <math>x</math> is loved, while <math>f(x)</math> yields the animal (if any) that <math>x</math> doesn't love. The 3rd last line from below then reads as ''"<math>x</math> doesn't love the animal <math>f(x)</math>, or else <math>x</math> is loved by <math>g(x)</math>"''.

The 2nd last line from above, <math>(\mathrm{Animal}(f(x)) \lor \mathrm{Loves}(g(x), x)) \land (\lnot \mathrm{Loves}(x, f(x)) \lor \mathrm{Loves}(g(x), x))</math>, is the CNF.

==See also==
* [[Algebraic normal form]]
* [[Conjunction/disjunction duality]]
* [[Disjunctive normal form]]
* [[Horn clause]] – A Horn clause is a disjunctive [[clause (logic)|clause]] (a [[disjunction]] of [[literal (mathematical logic)|literals]]) with at most one positive, i.e. [[negation|unnegated]], literal.
* [[Quine&ndash;McCluskey algorithm]]

== Notes ==
{{reflist}}

==References==
{{refbegin}}
* {{Cite book
|last=Andrews
|first=Peter B.
|year=2013
|title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
|publisher=Springer
|isbn=978-9401599344
}}
*{{cite book
|last=Howson
|first=Colin
|author-link=Colin Howson
|title=Logic with trees: an introduction to symbolic logic
|url=https://books.google.com/books?id=Y4WGAgAAQBAJ&q=%22conjunctive+normal+form%22
|date=11 October 2005
|orig-date=1997
|publisher=Routledge
|isbn=978-1-134-78550-6
}}
* {{Cite conference
|last1=Jackson
|first1=Paul
|last2=Sheridan
|first2=Daniel
|url=https://homepages.inf.ed.ac.uk/pbj/papers/sat04-bc-conv.pdf
|title=Clause Form Conversions for Boolean Circuits
|editor1-last=Hoos
|editor1-first=Holger H.
|editor2-last=Mitchell
|editor2-first=David G.
|book-title=Theory and Applications of Satisfiability Testing
|conference=7th International Conference on Theory and Applications of Satisfiability Testing, SAT
|conference-url=https://link.springer.com/book/10.1007/11527695
|date=10 May 2004
|location=Vancouver, BC, Canada
|pages=183{{ndash}}198
|series=Revised Selected Papers. Lecture Notes in Computer Science
|volume=3542
|publisher=Springer 2005
|doi=10.1007/11527695_15
|isbn=978-3-540-31580-3 <!-- Print: 978-3-540-27829-0 -->
}}
* {{cite book
|last1=Kleine Büning
|first1=Hans
|last2=Lettmann
|first2=Theodor
|date=28 August 1999
|title=Propositional Logic: Deduction and Algorithms
|url=https://books.google.com/books?id=3oJE9yczr3EC&q=%22conjunctive+normal+form%22
|publisher=[[Cambridge University Press]]
|isbn=978-0-521-63017-7
}}
* {{Cite book
|editor1-last=Russel
|editor1-first=Stuart
|editor1-link=Stuart J. Russell
|editor2-last=Norvig
|editor2-first=Peter
|editor2-link=Peter Norvig
|date=2010
|orig-date=1995
|title=Artificial Intelligence : A Modern Approach
|url=https://people.engr.tamu.edu/guni/csce421/files/AI_Russell_Norvig.pdf
|edition=3rd
|publisher=Prentice Hall
|location=Upper Saddle River, NJ
|isbn=978-0-13-604259-4
|archive-url=https://web.archive.org/web/20170831090316/https://pdfs.semanticscholar.org/bef0/731f247a1d01c9e0ff52f2412007c143899d.pdf
|archive-date=31 August 2017
|url-status=live
}}
* {{Cite book
|last=Tseitin
|first=Grigori S.
|author-link=Grigori Tseitin
|year=1968
|chapter=On the Complexity of Derivation in Propositional Calculus
|chapter-url=http://www.decision-procedures.org/handouts/Tseitin70.pdf
|editor-last=Slisenko
|editor-first=A.O.
|title=Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian)
|pages=115–125
|publisher=Steklov Mathematical Institute
}}
* {{cite book
|last=Whitesitt
|first=J. Eldon
|date=24 May 2012
|orig-year=1961
|title=Boolean Algebra and Its Applications
|url=https://books.google.com/books?id=20Un1T78GlMC&q=%22conjunctive+normal+form%22
|publisher=Courier Corporation
|isbn=978-0-486-15816-7
}}
{{refend}}

==External links==
* {{springer
|title=Conjunctive normal form
|id=p/c025090
}}

* {{Cite web
|url=https://www.mathematik.uni-marburg.de/~thormae/lectures/ti1/code/normalform/index.html
|title=Java tool for converting a truth table into CNF and DNF
|at=[https://www.uni-marburg.de/en/ Universität Marburg]
|access-date=31 December 2023
}}

[[Category:Normal forms (logic)]]
[[Category:Knowledge compilation]]
{{Normal forms in logic}}