Algorithm for Clause Form:

(‘A → B’ = rewrite A as B)

1. Convert wff to Prenex Normal Form: a) (P ⇔ Q) → ((P ⇒ Q) ∧ (Q ⇒ P))

b) (P ⇒ Q) → (¬P ∨ Q)

c) repeat: (i) ¬¬P → P (ii) ¬(P ∧ Q) → (¬P ∨ ¬Q) (iii) ¬(P ∨ Q) → (¬P ∧ ¬Q)

(iv) ¬∃x[α] → ∀x[¬α]
(v) ¬∀x[α] → ∃x[¬α]

until: ‘¬’ only applies to atomic wffs

d) Rename vars s.t. vars bound by diff qfrs have unique names

e) Move all qfrs left, w/o changing order

2. Convert PNF to Skolem NF:

a) ∀x_{1} … ∀x_{n}∃y[α(y)] → ∀x_{1} … ∀x_{n}[α(f(x_{1}, …, x_{n}))]

3. Convert SNF to Conjunctive NF: a) ∀x[α(x)] → α(x)

b) repeat: (P ∨ (Q ∧ R)) → ((P ∨ Q) ∧ (P ∨ R)) until: wff is a conjn of disjns of literals

4. Convert CNF to Clause Form:

a) (P ∨ Q) → P Q; each P Q is a clause

b) (P ∧ Q) → {P, Q}

c) Rename vars s.t. each clause has diff vars