Definition
Disjunctive Normal Form (Propositional Logic)
A propositional formula is in disjunctive normal form (DNF) if it is a disjunction of conjunctions of literals — a disjunction of terms:
where each
is a literal, i.e. an atom or a negated atom. The degenerate cases count as well: a single conjunction ( ), a single literal ( ), and a single atom ( ) are all in DNF. Example:
Transformation
Every formula has an equivalent DNF (normal form existence). Rewriting applies the De Morgan’s rules, double negation elimination, and distributivity — for DNF one distributes
Worked transformation
Exponential Blow-up
Warning
As with CNF, some formulas have only exponentially large equivalent DNFs, e.g. nested equivalences such as
. Naming (the definitional transformation) avoids the blow-up by preserving satisfiability rather than equivalence.