Negation normal form: meaning and examples

A formula is in negation normal form (NNF) when NOT appears only directly on variables and the only other operators are AND and OR. It is the halfway point of every conversion to CNF or DNF.

To reach negation normal form, first eliminate the derived operators (->, <->, XOR, NAND, NOR), then push each negation inward with De Morgan's laws, NOT (X AND Y) becoming NOT X OR NOT Y and NOT (X OR Y) becoming NOT X AND NOT Y, and cancel double negations. The result keeps the structure of the original, only with the negations moved to the leaves, so it is often no longer than what it started from. CNF and DNF are both obtained from it by distribution.

The artefact on this page is NOT (A AND (B OR NOT C)), not in NNF because the outer NOT covers a compound. Pushing it inward gives NOT A OR NOT (B OR NOT C), then NOT A OR (NOT B AND C): that is the converter's DNF, 2 terms and 3 literals, reached by one De Morgan step, and already in negation normal form. The CNF, (NOT A OR NOT B) AND (NOT A OR C), 2 clauses and 4 literals, needs one further distribution. The 8-row table reads false only on rows 4, 6 and 7.

Negation normal form is what makes a formula readable in plain language, since a negated compound is hard to say and a negated variable is easy: “A is false, or B is false and C is true”. Programmers apply the same transformation when they rewrite !(a && b) as !a || !b. It is confused with CNF and DNF, which are stricter, and with a simplified form; NNF only relocates negations, it does not shorten anything.

Example

f := NOT (A AND (B OR NOT C)) · output

Exact checks

Always true (tautology)? No Counterexample: A = T, B = F, C = F · Exhaustively checked and solver cross-checked · 5 rows

Always false (contradiction)? No Counterexample: A = F, B = F, C = F · Exhaustively checked and solver cross-checked · 1 rows

Can be true? Yes Example assignment: A = F, B = F, C = F · Exhaustively checked and solver cross-checked · 1 rows

Truth table (8 rows)

Negation normal form: meaning and examples
#	A	B	C	f
0	FALSE	FALSE	FALSE	TRUE
1	FALSE	FALSE	TRUE	TRUE
2	FALSE	TRUE	FALSE	TRUE
3	FALSE	TRUE	TRUE	TRUE
4	TRUE	FALSE	FALSE	FALSE
5	TRUE	FALSE	TRUE	TRUE
6	TRUE	TRUE	FALSE	FALSE
7	TRUE	TRUE	TRUE	FALSE

Plain-language reading

Beginnerf is true exactly when the following condition does not hold:
1. both of the following hold:
1.1. A is true
1.2. B is true or C is false (or both)
In every other case, f is false.
About the operators:
- NOT reverses a value: true becomes false and false becomes true.
- AND is true only when all of its parts are true.
- OR is inclusive: it is true when at least one part is true, including when several are.

Intermediatef is true exactly when the following condition does not hold:
1. both of the following hold:
1.1. A is true
1.2. B is true or C is false (or both)
In every other case, f is false.

Advancedf is true exactly when the following condition does not hold [negation ¬]:
1. both of the following hold [conjunction ∧]:
1.1. A is true
1.2. B is true or C is false (or both) [inclusive disjunction ∨]
In every other case, f is false.
Formal notation: ¬(A ∧ (B ∨ ¬C))

Normal forms

Conjunctive normal form (CNF)

(NOT A OR NOT B) AND (NOT A OR C)

2 clauses, 4 literals · complete · De Morgan's law ×1, Distribution ×1

Disjunctive normal form (DNF)

NOT A OR (NOT B AND C)

2 terms, 3 literals · complete · De Morgan's law ×1

The common slip

Pushing a negation through AND without flipping it to OR. NOT (A AND B) is NOT A OR NOT B, not NOT A AND NOT B; the second form is NOT (A OR B). The De Morgan pitfall page shows the two compared on every row.

Questions

Is every formula in CNF or DNF also in NNF?

Yes. Both forms allow negation only on literals and use only AND and OR, so they satisfy the NNF conditions. The converse fails: A AND (B OR (C AND D)) is in NNF but in neither CNF nor DNF.

Practice

De Morgan's law exercises with answers

Glossary

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.