Conjunctive normal form

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. 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 , and are in conjunctive normal form: For clarity, the disjunctive clauses are written inside parentheses above. In disjunctive normal form with parenthesized conjunctive clauses, the last case is the same, but the next to last is . The constants true and false are denoted by the empty conjunct and one clause consisting of the empty disjunct, but are normally written explicitly. The following formulas are not in conjunctive normal form: since an OR is nested within a NOT since an AND is nested within an OR Every formula can be equivalently written as a formula in conjunctive normal form. The three non-examples in CNF are: Every propositional formula can be converted into 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. Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF.