Editing Conjunctive normal form (section)

==Definition==
A logical formula is considered to be in CNF if it is a [[logical conjunction|conjunction]] of one or more [[logical disjunction|disjunctions]] of one or more [[literal (mathematical logic)|literals]]. As in [[disjunctive normal form]] (DNF), the only propositional operators in CNF are [[logical disjunction|or]] (<math>\vee</math>), [[logical conjunction|and]] (<math>\and</math>), and [[negation|not]] (<math>\neg</math>). 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:
: ''CNF'' <math>\, \to \,</math> ''Disjunct'' <math>\, \mid \, </math> ''Disjunct'' <math>\, \land \,</math> ''CNF''
: ''Disjunct'' <math>\, \to \,</math> ''Literal'' <math>\, \mid\, </math> ''Literal'' <math>\, \lor \,</math> ''Disjunct''
: ''Literal'' <math>\, \to \,</math> ''Variable'' <math>\, \mid \,</math> <math>\, \neg \,</math> ''Variable''
Where ''Variable'' is any variable.

All of the following formulas in the variables <math>A,B,C,D,E,</math> and <math>F</math> are in conjunctive normal form:

* <math>(A \lor \neg B \lor \neg C) \land (\neg D \lor E \lor F \lor D \lor F)</math>
* <math>(A \lor B) \land (C)</math>
* <math>(A \lor B)</math>
* <math>(A)</math>

The following formulas are '''not''' in conjunctive normal form:
* <math>\neg (A \land B)</math>, since an AND is nested within a NOT
*<math>\neg(A \lor B) \land C</math>, since an OR is nested within a NOT
* <math>A \land (B \lor (D \land E))</math>, since an AND is nested within an OR