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 = F _{1} &and F_{2} &and ... &and F_{n}*
where each

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