Literal in logic: meaning and examples

A literal is a variable or the negation of a variable: A and NOT B are literals, A AND B and NOT (A OR B) are not. Literals are the atoms from which clauses, terms and normal forms are built.

A positive literal is a plain variable; a negative literal is a variable under a single NOT. The negation must sit directly on the variable: NOT (A AND B) is not a literal until De Morgan has pushed the negation inward, which is what negation normal form does. Every clause is an OR of literals, every product term is an AND of literals, and the size of a normal form is usually measured by counting its literals, as the CNF/DNF converter does with its literal count.

The artefact on this page is (A OR NOT B) AND (B OR C), which contains four literals: A, NOT B, B and C, B appearing in both polarities. The converter reports it already in conjunctive normal form, 2 clauses and 4 literals with no law applied, and gives the disjunctive normal form (A AND B) OR (A AND C) OR (NOT B AND C), 3 terms and 6 literals, reached with one use of distribution and one of the complement law. The satisfiable check holds with the witness A = FALSE, B = FALSE, C = TRUE.

Literal counts are the usual cost measure in hardware (each literal is a gate input) and in SAT solving (the input format of a solver is a list of clauses of literals). In testing, each literal is a condition that MC/DC asks to be shown independently affecting the outcome. The term is confused with a constant (TRUE and FALSE are not literals in this sense) and with a string literal in a programming language, which is unrelated.

Example

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

Exact checks

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

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

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

Truth table (8 rows)

Literal in logic: meaning and examples
#	A	B	C	f
0	FALSE	FALSE	FALSE	FALSE
1	FALSE	FALSE	TRUE	TRUE
2	FALSE	TRUE	FALSE	FALSE
3	FALSE	TRUE	TRUE	FALSE
4	TRUE	FALSE	FALSE	FALSE
5	TRUE	FALSE	TRUE	TRUE
6	TRUE	TRUE	FALSE	TRUE
7	TRUE	TRUE	TRUE	TRUE

Plain-language reading

Beginnerf is true exactly when both of the following hold:
1. A is true or B is false (or both)
2. at least one of B or C is true (both may be true)
In every other case, f is false.
About the operators:
- 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.
- NOT reverses a value: true becomes false and false becomes true.

Intermediatef is true exactly when both of the following hold:
1. A is true or B is false (or both)
2. at least one of B or C is true (both may be true)
In every other case, f is false.

Advancedf is true exactly when both of the following hold [conjunction ∧]:
1. A is true or B is false (or both) [inclusive disjunction ∨]
2. at least one of B or C is true (both may be true) [inclusive disjunction ∨]
In every other case, f is false.
Formal notation: (A ∨ ¬B) ∧ (B ∨ C)

Normal forms

Conjunctive normal form (CNF)

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

2 clauses, 4 literals · complete

Disjunctive normal form (DNF)

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

3 terms, 6 literals · complete · Distribution ×1, Complement ×1

The common slip

Counting B and NOT B as one literal. They are two different literals of the same variable, and a clause containing both is a tautology that the complement law removes. The literal count on this page is 4, not 3, for exactly that reason.

Questions

Is NOT NOT A a literal?

Not as written: a literal has at most one negation directly on the variable. Double negation reduces NOT NOT A to the positive literal A, and the normal-form converter applies that law before counting.

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.