Normal Forms

A literal is an atom or negation of an atom: P or ¬ P.

A formula F is in conjunctive normal form (CNF) if F is of the form F = F1 &and F2 &and ... &and Fn where each Fi is a disjunction of literals. Example: (¬ P &or Q) &and (P) &and (¬ Q)

CNF is used for resolution, so it is the one we will use. There is also a disjunctive normal form.

Contents    Page-10    Prev    Next    Page+10    Index