Conjunctive Normal Form

In Conjunctive Normal Form (CNF), propositions are represented as CONJUNCTIONS of DISJUNCTIONS of LITERALS (a literal is an atomic proposition or its negation).
Example: (p ∨ Nr) ∧ (Nq ∨ Nr ∨ s) ∧ (s ∨ q)
In CNF, the topmost operator is the universal conjunction operator, and the only other operators are ∨ and ¬.

Some terminology: a clause is a proposition whose topmost operator is universal disjunction. A clause is here represented as a list of propositions (e.g., [p, Cpq, r]). A clause set is the universal conjunction of a set of clauses. Clause sets are indicated with angled bracks (e.g.,〈[p, Cpq, r],[ApNq,Nr]〉).

To convert a proposition into CNF, we follow two types of rules: α rules, like ∧-elimination, which add a new clause to the clause set; and, β rules, like ∨-elimination, which add new propositions to the same clause.