In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.

In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.

A logical formula is considered to be in CNF if it is a conjunction of one or more disjunctions of one or more literals. As in disjunctive normal form (DNF), the only propositional operators in CNF are or (${\displaystyle \vee }$), and (${\displaystyle \land }$), and not (${\displaystyle \neg }$). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

The following is a context-free grammar for CNF:

Where Variable is any variable.

All of the following formulas in the variables ${\displaystyle A,B,C,D,E,}$ and ${\displaystyle F}$ are in conjunctive normal form:

The following formulas are not in conjunctive normal form:

In classical logic each propositional formula can be converted to an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.