Lecture #13, Oct. 30
Resolution
Easy and self-documenting 2-dimensional proofs.
The technique is used in the “automatic theorem proving”, i.e., special computer systems (programs) that prove theorems.
It is based on proof by contradiction metatheorem:
0.0.1 Metatheorem.
iff
Γ, ¬A ⊢ ⊥ (1) Γ⊢A (2)
Thus, instead of proving (2) prove (1).
(1) is proved using (almost) exclusively the CUT Rule.
1
The technique can be easily learnt via examples:
Basic Logic© by George Tourlakis
2
0.0.2 Example. Use Resolution to prove (1) below:
A → B, C → D ⊢ A ∨ C → B ∨ D (1)
by DThm prove instead:
A → B, C → D, A ∨ C ⊢ B ∨ D
By 0.0.1 prove instead that the “Γ” in the top line below proves ⊥
Basic Logic© by George Tourlakis
0.0.3 Example. Next prove
⊢ (A → (B → C)) → ((A → B) → (A → C))
By the DThm prove instead
A → (B → C) ⊢ (A → B) → (A → C)
Two more applications of the DThm simplify what we will prove into the following: A → (B → C),A → B,A ⊢ C
By 0.0.1, prove instead that Γ ⊢ ⊥ where
Γ = {¬A ∨ ¬B ∨ C, ¬A ∨ B, A, ¬C}
3
Basic Logic© by George Tourlakis
4
0.0.4 Example. Prove ByDThmdoinsted: A∧¬B⊢¬(A→B).
By 0.0.1 do instead or
A ∧ ¬B, A → B ⊢ ⊥ A ∧ ¬B, ¬A ∨ B ⊢ ⊥
Use HYP Splitting, so do instead
A, ¬B, ¬A ∨ B ⊢ ⊥ A,¬B,¬A∨B
To this end, cut 1st and 3rd to get B. Cut the latter with ¬B to get ⊥.
0.0.5 Example.
¬(A∨B)
¬A∧¬B ¬A ¬B
Basic Logic© by George Tourlakis
⊢ (A ∧ ¬B) → ¬(A → B)
Bibliography
[Rob65] J.A. Robinson, A Machine Oriented Logic Based on the Resolution Princi- ple, JACM 12 (1965), no. 1, 23–41.
Basic Logic© by George Tourlakis