Normal forms Glossary
Definition
A formula
of propositional logic
is in negation normal form (NNF)
iff:
(i) The
only connectives in it are
AND, OR
and NOT
(ii) No binary connective
occurs inside the scope of
NOT.
A formula is in conjunctive
normal form (CNF) iff:
(i) It is in negation normal form
(ii) No AND is inside the
scope of any OR.
A formula is in disjunctive normal
form (DNF) iff:
(i) It is in negation normal form
(ii) No OR is inside the
scope of any AND.
Comments
Literal: It is sometimes useful to have a word meaning "atom or negated atom". We call such a formula a literal. Its complementary literal is the literal resulting from it by adding or deleting the negation connective.
Clause A clause is a disjunction of [one or more] literals. So a formula in CNF is a conjunction of [one or more] clauses. For this reason, CNF is sometimes called "clause form". For some purposes it is useful to include the absurd constant ⊥ as the empty clause, consisting of zero literals.
Every formula has an equivalent in CNF (and an equivalent in DNF). This fact is heavily used in automated reasoning, as it means that algorithms for reasoning with clauses are sufficient to do the whole of logic.
Examples
- p AND (q OR (NOTp AND NOTr) is in NNF, but not in CNF or DNF.
- (p AND q) OR (NOTp AND NOTr) is in DNF.
- (p OR q) AND (NOTp OR NOTr) is in CNF.