Normal forms
Rewrite a propositional formula into a conjunction of disjunctions of literals (CNF) or a disjunction of conjunctions of literals (DNF). Each rewrite preserves equivalence.
Scope. One propositional formula at a time. For first-order preprocessing, see Skolemization .
Step through
Ex.
The interactive example is loading.
Text tree
Work it yourself
Choose a level to begin.
Using it
Choose CNF or DNF and step through the local rewrites. Rewriting proceeds from the root outwards, left to right. Repeated terms remain visible.
In Work it yourself, enter the formula, then supply an equivalent DNF and CNF. Check verifies their shape and truth-values. A failed equivalence check gives a valuation where the formulas differ.
In the book
- Chapter 5 · Normal forms defines the two shapes and the literals they are built from.
- Chapter 5 · Rewriting a formula gives the equivalences and the order to apply them in.
- Chapter 4 · Boolean laws is where those equivalences come from.