• Back to Profile

  • Die Logik ist keine Lehre, sondern ein Spiegelbild der Welt.
    Logik ist transzendental.

    - Ludwig Wittgenstein's (1921, 6.13) Tractatus Logico-Philosophicus in the original German

    Logic is not a body of doctrine, but a mirror-reflection of the world.
    Logic is transcendental.
    - Pears/McGuinness translation

    Proof by Resolution


    Carlo Innocenzo Carlone's (1745-7) The Triumph of Reason



    1. Resolution is a proof theory that works on expressions in clausal form
    2. Resolution does not rely on any rules of inference (e.g. modus ponens, modus tollens, etc) apart from the Resolution Principle
    3. Proof by resolution is employed in automated theorem proving
    4. NOTE: There is almost universal consensus that proof by natural deduction rather than proof by resolution is the proof theory of choice

    φDR ψ

    1. The mode of inference is deductive (represented by the superscript D)
    2. The inferential mechanism is proof by resolution (represented by the subscript R)

    1. STEP 1: The premises and conclusions must be converted into clausal form before the Resolution Principle is applied
    2. 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}


    1. STEP 2: Apply the Resolution Principle
    2. According to this principle:
    3. 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 ~λ

    4. STEP 3: Derive the empty clause
    5. The empty clause is also a clause, equivalent to an empty disjunction
    6. The derivation of an empty clause (i.e. a clause containing no literals) means that the database contains a contradiction

    7. STEP 4: Conclude the proof





    1. EXAMPLE 1:
    2. P1: p → q
    3. C: ∴ ∼q → ∼p
    4. Prove that this argument is valid.
    1. Proof by resolution:
    2. 1. {~p, q} (see STEP 1)
    3.    ∼q → ∼p
    4. 2.      asm: {~q}, {p} (assume negation of conclusion and convert to clausal form; see STEP 1)
    5. 3.      ∴ {p} (from 2)
    6. 4.      ∴ {~q} (from 2)
    7. 5.      ∴ {q} (from 1 & 3, apply the Resolution Principle) (see STEP 2)
    8. 6.      ∴ {} (from 4 & 5, 3 apply the Resolution Principle and derive the empty clause) (see STEPS 2 & 3)
    9. 7.    ∴ {q, ~p} (or ∼q → ∼p)

    10. We have a 7-line proof by resolution of the validity of the argument in EXAMPLE 1