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 conjunctions. More simply stated, the outermost operators of the formula are all ORs, and there is only one level of nesting allowed, which may only can literals or conjunctions of literals. For example, all of the following formulas are in DNF:

A ∨ B
A
(A ∧ B) ∨ C
(A ∧ ¬B &and ¬C) &or (¬D ∧ E ∧ F)

However, the following formulas are not in DNF:

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

Note that all logical formulas can be converted into disjunctive normal form. A formal grammar for DNF is as follows:

1. o -> ∨
2. a -> ∧
3. n -> ¬
4. A -> B
5. A -> A o B
6. B -> C
7. B -> (B a C)
8. C -> D
9. C -> nD
10. D -> term

See Also:

• Conjunctive normal form