In Boolean logic, 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. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

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.

Definition

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 \wedge }$), 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:

1. CNF → (Disjunction) ${\displaystyle \land }$ CNF
2. CNF → (Disjunction)
3. Disjunction → Literal ${\displaystyle \lor }$ Disjunction
4. Disjunction → Literal
5. Literal → ${\displaystyle \neg }$Variable
6. Literal → Variable

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:

• ${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F\lor D\lor F)}$
• ${\displaystyle (A\lor B)\land (C)}$
• ${\displaystyle (A\lor B)}$
• ${\displaystyle (A)}$

The following formulas are not in conjunctive normal form:

• ${\displaystyle \neg (A\land B)}$, since an AND is nested within a NOT
• ${\displaystyle \neg (A\lor B)\land C}$, since an OR is nested within a NOT
• ${\displaystyle A\land (B\lor (D\land E))}$, since an AND is nested within an OR

Conversion to CNF

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

Basic algorithm

The algorithm to compute a CNF-equivalent of a given propositional formula ${\displaystyle \phi }$ builds upon ${\displaystyle \lnot \phi }$ in disjunctive normal form (DNF): step 1.^[2]
Then ${\displaystyle \lnot \phi _{DNF}}$ is converted to ${\displaystyle \phi _{CNF}}$ by swapping ANDs with ORs and vice versa while negating all the literals. Remove all ${\displaystyle \lnot \lnot }$.^[1]

Conversion by syntactic means

Convert to CNF the propositional formula ${\displaystyle \phi }$.

Step 1: Convert its negation to disjunctive normal form.^[2]

${\displaystyle \lnot \phi _{DNF}=(C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})}$,^[a]

where each ${\displaystyle C_{i}}$ is a conjunction of literals ${\displaystyle l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}}}$.^[b]

Step 2: Negate ${\displaystyle \lnot \phi _{DNF}}$. Then shift ${\displaystyle \lnot }$ inwards by applying the (generalized) De Morgan's equivalences until no longer possible.

$${\displaystyle {\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot (C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})\\&\leftrightarrow \lnot C_{1}\land \lnot C_{2}\land \ldots \land \lnot C_{i}\land \ldots \land \lnot C_{m}&&{\text{// (generalized) D.M.}}\end{aligned}}}$$

$${\displaystyle {\begin{aligned}\lnot C_{i}&=\lnot (l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}})\\&\leftrightarrow (\lnot l_{i1}\lor \lnot l_{i2}\lor \ldots \lor \lnot l_{in_{i}})&&{\text{// (generalized) D.M.}}\end{aligned}}}$$

Step 3: Remove all double negations.

Example

Convert to CNF the propositional formula ${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}=((\mathrm{\neg <!--\; \neg \; -->}(p\wedge <!--\; \wedge \; -->q))\leftrightarrow <!--\; \leftrightarrow \; -->(}$Zdroj:https://en.wikipedia.org?pojem=Clause_normal_form
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.