 STEP 1: The premises and conclusions must be converted into clausal form before the Resolution Principle is applied
 Each clause is either a literal (e.g. p, ~p, q, ~q, etc) or a disjunction of literals
Logical formula

Conversion to clausal form

Representation

p → q (material conditional)

∼p ∨ q

{∼p, q}

p ⟷ q (material biconditional)

(∼p ∨ q) ∧ (∼q ∨ p)

{∼p, q},{∼q, p}

∼(p ∧ q) (negation)

∼p ∨ ∼q

{∼p, ∼q}

∼(p ∨ q) (negation)

∼p ∧ ∼q

{∼p},{∼q}

p ∨ (q ∧ r) (distribution)

(p ∨ q) ∧ (p ∨ r)

{p, q}, {p, r}

(p ∧ q) ∨ r (distribution)

(p ∨ r) p ∧ (q ∨ r)

{p, r}, {q, r}

⋮

⋮

⋮

 STEP 2: Apply the Resolution Principle
 According to this principle:
 Given a clause containing a literal λ and another clause containing its negation ~λ, we can infer the clauses containing all the literals of both clauses without the complementary pair λ and ~λ
 STEP 3: Derive the empty clause
 The empty clause is also a clause, equivalent to an empty disjunction
 The derivation of an empty clause (i.e. a clause containing no literals) means that the database contains a contradiction
 STEP 4: Conclude the proof

 Proof by resolution:
 1. {~p, q} (see STEP 1)
 ∼q → ∼p
 2. asm: {~q}, {p} (assume negation of conclusion and convert to clausal form; see STEP 1)
 3. ∴ {p} (from 2)
 4. ∴ {~q} (from 2)
 5. ∴ {q} (from 1 & 3, apply the Resolution Principle) (see STEP 2)
 6. ∴ {} (from 4 & 5, 3 apply the Resolution Principle and derive the empty clause) (see STEPS 2 & 3)
 7. ∴ {q, ~p} (or ∼q → ∼p)
 We have a 7line proof by resolution of the validity of the argument in EXAMPLE 1
