This post discusses seven normal forms:
- Negation normal form
- Conjunctive normal form
- Disjunctive normal form
- Algebraic normal form
- Prefix normal form
- Skolem normal form
- Blake canonical form
The photo above is Thoralf Skolem, Norwegian mathematician and author of Skolem normal form.
Negation normal form
The only symbols in negation normal form are conjunction (∧), disjunction (∨), and negation (¬). Also, negation only applies to variables, i.e. not to a clause.
So, for example,
a → b
is not in negation normal form because it contains the symbol “→” but it is equivalent to
¬ a ∨ b
which is in negation normal form. Similarly,
¬(a ∨ b)
is not in negation normal form because the negation operator is applied to more than a variable. But by De Morgan’s laws the expression is equivalent to
¬a ∧ ¬b.
which again is in negation normal form.
Conjunctive normal form
A formula is in conjunctive normal form (CNF) if it is an AND of ORs. That is, it is the conjunction of terms containing only disjunctions of variables.
For example,
(a ∧ b) ∨ c
fails to be in CNF for two reasons. First, the two clauses are OR’d together, not AND’d together. Second, the variables in the first clause are AND’d together, not OR’d together. So what we have here is a sort of opposite of conjunctive normal form called disjunctive normal form which we discuss in the next section.
The formula above is equivalent to
(a ∨ c) ∧ (b ∨ c)
which is in CNF.
The satisfiability problem (SAT) is NP-complete when clauses have three or more variables, but SAT is easy for expressions in conjunctive normal form. The catch is that the problem of putting a general expression in CNF is NP-complete.
Disjunctive normal form
Disjunctive normal form (DNF) is the dual of conjunctive normal form, and OR of ANDs rather than an AND of ORs, such as the expression
(a ∧ b) ∨ c
from the section above.
Algebraic normal form
A Boolean expression is in algebraic normal form if it consists of the constants 0 and 1, variables, XOR, and AND.
XOR is written with ⊕ and AND is written as multiplication, i.e. juxtaposition.
To put an expression in ANF, you can XOR with 1 to eliminate negation, i.e.
¬a = 1⊕a.
Also, you can eliminate ORs by using
a ∨ b = 1⊕(1⊕a)(1⊕b).
Prenex normal form
A formula in predicate logic is in prenex normal form (PNF) if all the quantifiers come first. For example,
∀ ε ∃ δ(…)
is in PNF as long as there are no quantifiers, no ∀ or ∃ operators, in the parenthesized part.
Skolem normal form
Skolem normal form is a special case of prenex normal form in which all the existential quantifiers come before any universal quantifiers, i.e. all the ∃’s come before the ∀’s. Skolemization, the process of putting an expression in Skolem normal form, is an important technique in automated theorem proving.
Blake canonical form
Blake canonical form (BCF) is a special case of disjunctive normal form. It too is a disjunction of clauses, but the clauses are required to be prime implicants.
Think of a logical formula as a Boolean function f. An implicant of f is a function g such that every choice of variable values that makes g return 1 also makes f return 1. A prime implicant is one that contains no unnecessary variables, i.e. if you remove any variable the function is no longer an implicant of f.