Disjunctive normal form

Disjunctive Normal Form or DNF is a method of standardizing and normalizing logical formulas. A logical formula is considered to be in DNF if and only if it is a single disjunction of conjunctionss. More simply stated, the outermost operators of the formula are all ORs, and there is only one level of nesting allowed, which may only contain literals or conjunctions of literals. For example, all of the following formulas are in DNF:

A ∨ B
A
(A ∧ B) ∨ C
(A ∧ ¬B ∧ ¬C) ∨ (¬D ∧ E ∧ F)

However, the following formulas are not in DNF:

¬(A ∨ B) — NOT is the outermost operator
A ∨ (B ∧ (C ∨ D)) — an OR is nested within an AND

Note that all logical formulas can be converted into disjunctive normal form. However, in some cases conversion to DNF can lead to an exponential explosion of the formula. For example, in DNF form, logical formulas of the following form have 2^n terms:

(X1 ∨ Y1) ∧ (X2 ∨ Y2) ∧ ... ∧ (Xn ∨ Yn)

The following is a formal grammar for DNF:

<or> -> ∨
<and> -> ∧
<not> -> ¬
<disjunct> -> <conjunct>
<disjunct> -> <disjunct> <or> <conjunct>
<conjunct> -> <literal>
<conjunct> -> (<conjunct> <and> <literal>)
<literal> -> <term>
<literal> -> <not><term>

Where <term> is any variable.