Editing Disjunctive normal form (section)

==Definition==
A logical formula is considered to be in DNF if it is a [[logical disjunction|disjunction]] of one or more [[logical conjunction|conjunctions]] of one or more [[literal (mathematical logic)|literals]].{{sfn|Davey|Priestley|1990|page=153}}{{sfn|Gries|Schneider|1993|page=67}}{{sfn|Whitesitt|2012|pages=33-37}} A DNF formula is in '''full disjunctive normal form''' if each of its variables appears exactly once in every conjunction and each conjunction appears at most once (up to the order of variables). As in [[conjunctive normal form]] (CNF), the only propositional operators in DNF are [[logical conjunction|and]] (<math>\wedge</math>), [[logical disjunction|or]] (<math>\vee</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 DNF:
: ''DNF'' <math>\, \to \,</math> ''Conjunct'' <math>\, \mid \, </math> ''Conjunct'' <math>\, \lor \,</math> ''DNF''
: ''Conjunct'' <math>\, \to \,</math> ''Literal'' <math>\, \mid\, </math> ''Literal'' <math>\, \land \,</math> ''Conjunct''
: ''Literal'' <math>\, \to \,</math> ''Variable'' <math>\, \mid \,</math> <math>\, \neg \,</math> ''Variable''
Where ''Variable'' is any variable.

For example, all of the following formulas are in DNF:

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

The formula <math>A \lor B</math> is in DNF, but not in full DNF; an equivalent full-DNF version is <math>(A \land B) \lor (A \land \lnot B) \lor (\lnot A \land B)</math>.

The following formulas are '''not''' in DNF:
*<math>\neg(A \lor B)</math>, since an OR is nested within a NOT
*<math>\neg(A \land B) \lor C</math>, since an AND is nested within a NOT
*<math>A \lor (B \land (C \lor D))</math>, since an OR is nested within an AND<ref>However, this one is in [[negation normal form]].</ref>