Conjunctive normal form

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of clauses, where a clause is a disjunction of literals; otherwise put, it is an AND of ORs. As a normal form, it is useful in automated theorem proving. It is similar to the 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 or a predicate symbol.

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.

All of the following formulas in the variables A, B, C, D, and E are in conjunctive normal form:

The third formula is in conjunctive normal form because it can be seen as the conjunction of the two single-literal clauses ${\displaystyle A}$ and ${\displaystyle B}$. Incidentally, the last two formulas are also in disjunctive normal form.

...
Wikipedia