Conjunctive normal form

related topics
{math, number, function}
{law, state, case}

In Boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals, where a literal and its complement cannot appear in the same clause.[citation needed] As a normal form, it is useful in automated theorem proving. It is similar to the canonical product of sums form used in circuit theory.

All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and conjunctions of a single clause, respectively. As in the disjunctive normal form (DNF), the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

Contents

Examples and counterexamples

All of the following formulas are in CNF:

The last formula is in CNF because it can be seen as the conjunction of the two single-literal clauses A and B. Incidentally, this formula is also in disjunctive normal form. The following formulae are not in CNF:

The above three formulae are respectively equivalent to the following three formulas that are in CNF:

Conversion into CNF

Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: the double negative law, De Morgan's laws, and the distributive law.

Since all logical formulae can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF. However, in some cases this conversion to CNF can lead to an exponential explosion of the formula. For example, translating the following non-CNF formula into CNF produces a formula with 2n clauses:

Full article ▸

related documents
Axiom of regularity
Generalized Riemann hypothesis
Monotonic function
Cartesian product
Algebraic topology
Diffeomorphism
Laurent series
Isomorphism theorem
Kolmogorov space
Tree (data structure)
Diophantine set
Well-order
Differential topology
Discriminant
Knight's tour
Goodstein's theorem
Carmichael number
Lebesgue measure
Group representation
Mean value theorem
Local ring
Controllability
Convex set
Spectrum of a ring
Product topology
Theory of computation
De Morgan's laws
Euler's totient function
Kruskal's algorithm
Cauchy-Riemann equations