Clause in logic: meaning and examples

Q: When is a clause a tautology?

When it contains a variable and its negation, such as A OR NOT A OR C: one of the two literals is always true. The complement law removes such clauses from a conjunctive normal form, since AND-ing with TRUE changes nothing.

A clause is an OR of literals, such as A OR NOT B. A formula in conjunctive normal form is an AND of clauses, and a clause is satisfied by any assignment that makes at least one of its literals true.

In the strict sense used by normal forms and SAT solvers, a clause is a disjunction: a list of literals joined by OR, satisfied when any one of them holds and falsified only when all of them are false. A clause with one literal is a unit clause, and the empty clause is a contradiction. Some authors use “clause” for any sub-formula or for an AND-term as well; this reference keeps the strict meaning and uses “term” for an AND of literals.

The artefact on this page is (A OR NOT B) AND (B OR C), an AND of two clauses, A OR NOT B and B OR C. The converter reports it already in conjunctive normal form, 2 clauses, 4 literals, no law applied, and derives the disjunctive form (A AND B) OR (A AND C) OR (NOT B AND C), 3 terms and 6 literals, by one distribution and one complement step. Row 0, A = FALSE, B = FALSE, C = FALSE, falsifies the second clause and is the tautology counterexample.

Clauses are the native unit of SAT solving: a solver's input is a set of clauses, and resolution works by combining two clauses on a complementary pair of literals. They also describe constraints naturally, since each clause is one requirement that must hold. The term is confused with a product term, with a sub-expression in general, and with a clause of a legal document or a SQL statement, which share the word and nothing else.

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)

Clause 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

Calling the AND-terms of a sum of products “clauses”. In the normal-form vocabulary a clause is an OR of literals; the AND of literals is a term or product term. Mixing the words makes a CNF description read as a DNF one.

Questions

When is a clause a tautology?

When it contains a variable and its negation, such as A OR NOT A OR C: one of the two literals is always true. The complement law removes such clauses from a conjunctive normal form, since AND-ing with TRUE changes nothing.

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.