Conjunctive Normal Form

See: Conjunctive Normal Form Logic Formula, Disjunctive Normal Form, Conjunction.

References

(Pfahringer, 2011a) ⇒ Bernhard Pfahringer. (2011). “Conjunctive Normal Form.” In: (Sammut & Webb, 2011) p.209

(Wikipedia, 2009) ⇒ http://en.wikipedia.org/wiki/Conjunctive_normal_form
- In boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals. As a normal form, it is useful in automated theorem proving. It is similar to the canonical 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 disjunctions 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.
CYC Glossary http://www.cyc.com/cycdoc/ref/glossary.html
- conjunctive normal form (CNF): A formula in CycL or first-order predicate calculus is in conjunctive normal form if it is a conjunction of disjunctions of literals. For example,