Editing Disjunctive normal form (section)

==Conversion to DNF==
In [[classical logic]] each propositional formula can be converted to DNF{{sfn|Davey|Priestley|1990|page=152-153}} ...
[[File:Karnaugh map KV 4mal4 18.svg|thumb|[[Karnaugh map]] of the disjunctive normal form {{color|#800000|(¬''A''∧¬''B''∧¬''D'')}} ∨ {{color|#000080|(¬''A''∧''B''∧''C'')}} ∨ {{color|#008000|(''A''∧''B''∧''D'')}} ∨ {{color|#800080|(''A''∧¬''B''∧¬''C'')}}]]
[[File:Karnaugh map KV 4mal4 19.svg|thumb|Karnaugh map of the disjunctive normal form {{color|#800080|(¬''A''∧''C''∧¬''D'')}} ∨ {{color|#008000|(''B''∧''C''∧''D'')}} ∨ {{color|#000080|(''A''∧¬''C''∧''D'')}} ∨ {{color|#800000|(¬''B''∧¬''C''∧¬''D'')}}. Despite the different grouping, the same fields contain a "1" as in the previous map.]]

=== ... by syntactic means ===
The conversion involves using [[logical equivalence]]s, such as [[double negation elimination]], [[De Morgan's laws]], and the [[Distributive property#Propositional logic|distributive law]]. Formulas built from the [[Functional completeness#Introduction|primitive]] [[Logical connective|connectives]] <math>\{\land,\lor,\lnot\}</math><ref>Formulas with other connectives can be brought into [[negation normal form]] first.</ref> can be converted to DNF by the following [[Abstract rewriting system|canonical term rewriting system]]:{{sfn|Dershowitz|Jouannaud|1990|page=270|loc=Sect.5.1}}
:<math>\begin{array}{rcl}
(\lnot \lnot x) & \rightsquigarrow & x \\
(\lnot (x \lor y)) & \rightsquigarrow & ((\lnot x) \land (\lnot y)) \\
(\lnot (x \land y)) & \rightsquigarrow & ((\lnot x) \lor (\lnot y)) \\
(x \land (y \lor z)) & \rightsquigarrow & ((x \land y) \lor (x \land z)) \\
((x \lor y) \land z) & \rightsquigarrow & ((x \land z) \lor (y \land z)) \\
\end{array}</math>

=== ... by semantic means ===
The full DNF of a formula can be read off its [[truth table]].<ref>{{harvnb|Smullyan|1968|p=14}}: "Make a truth-table for the formula. Each line of the table which comes out "T" will yield one of the basic conjunctions of the disjunctive normal form."</ref>{{sfn|Sobolev|2020}} For example, consider the formula
:<math>\phi = ((\lnot (p \land q)) \leftrightarrow (\lnot r \uparrow (p \oplus q)))</math>.<ref><math>\phi</math> = (('''[[Negation|NOT]]''' (p '''[[Logical conjunction|AND]]''' q)) '''[[If and only if|IFF]]''' (('''[[Negation|NOT]]''' r) '''[[Sheffer stroke|NAND]]''' (p '''[[XOR]]''' q)))</ref>

The corresponding [[truth table]] is
:{| class="wikitable" style="text-align:center;"
! <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>
|-
| T || T || T ||style="background:black"| || || F || T || || style="background:papayawhip" | F || || F || T || F ||
|-
| T || T || F ||style="background:black"| || || F || T || || style="background:papayawhip" | F || || T || T || F ||
|-
| style="background:lightgreen"|T || style="background:lightgreen"|F || style="background:lightgreen"|T ||style="background:black"| || || T || F || || style="background:papayawhip" | '''T''' || || F || T || T ||
|-
| T || F || F ||style="background:black"| || || T || F || || style="background:papayawhip" | F || || T || F || T ||
|-
| style="background:lightgreen"|F || style="background:lightgreen"|T || style="background:lightgreen"|T ||style="background:black"| || || T || F || || style="background:papayawhip" | '''T''' || || F || T || T ||
|-
| F || T || F ||style="background:black"| || || T || F || || style="background:papayawhip" | F || || T || F || T ||
|-
| style="background:lightgreen"|F || style="background:lightgreen"|F || style="background:lightgreen"|T ||style="background:black"| || || T || F || || style="background:papayawhip" | '''T''' || || F || T || F ||
|-
| style="background:lightgreen"|F || style="background:lightgreen"|F || style="background:lightgreen"|F ||style="background:black"| || || T || F || || style="background:papayawhip" | '''T''' || || T || T || F ||
|}

* The full DNF equivalent of <math>\phi</math> is
:<math>
(      p \land \lnot q \land       r) \lor
(\lnot p \land       q \land       r) \lor
(\lnot p \land \lnot q \land       r) \lor
(\lnot p \land \lnot q \land \lnot r)
</math>
* The full DNF equivalent of <math>\lnot \phi</math> is
:<math>
(      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>

=== Remark ===
A propositional formula can be represented by one and only one full DNF.{{refn|name="noreps"|It is assumed that repetitions and variations<ref>like <math>(a \land b) \lor (b \land a) \lor (a \land b \land b)</math></ref> based on the [[Commutative property|commutativity]] and [[Associative property|associativity]] of <math>\lor</math> and <math>\land</math> do not occur.}} In contrast, several ''plain'' DNFs may be possible. For example, by applying the rule <math>((a \land b) \lor (\lnot a \land b)) \rightsquigarrow b</math> three times, the full DNF of the above <math>\phi</math> can be simplified to <math>(\lnot p \land \lnot q) \lor (\lnot p \land r) \lor (\lnot q \land r)</math>. However, there are also equivalent DNF formulas that cannot be transformed one into another by this rule, see the pictures for an example.