- 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 7-line proof by resolution of the validity of the argument in EXAMPLE 1
|