cnf_resolution_soundness

theoremverified

Soundness of the resolution rule: for any truth assignment `τ : V → Bool`, variable `v : V`, and clauses `C, D : List (CnfLit V)`, if there exists a literal in `C ++ [CnfLit.pos v]` satisfied by `τ` (that is, `match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false`) and a literal in `D ++ [CnfLit.neg v]` satisfied by `τ`, then there exists a literal in `C ++ D` satisfied by `τ`.

Statement

theorem cnf_resolution_soundness {V : Type*} (τ : V → Bool) (v : V)
    (C D : List (CnfLit V))
    (hC : ∃ l ∈ C ++ [CnfLit.pos v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false)
    (hD : ∃ l ∈ D ++ [CnfLit.neg v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false) :
    ∃ l ∈ C ++ D, match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false

Source

Cook 1971, The complexity of theorem-proving procedures

Verified

07 Sep 2026

Axioms

propext

Built on 1

CnfLitA CNF literal over a variable type V is either a positive variable or a negated variable.

Read back from the Lean

For any type V, truth assignment τ : V → Bool, element v : V, and lists of literals C and D over V: if there exists a literal l in C ++ [CnfLit.pos v] that evaluates to true under τ (meaning τ u = true if l = CnfLit.pos u, and τ u = false if l = CnfLit.neg u), and there exists a literal l in D ++ [CnfLit.neg v] that evaluates to true under τ, then there exists a literal l in C ++ D that evaluates to true under τ.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- Soundness of the resolution rule: if an assignment satisfies both C ∨ v and D ∨ ¬v, it satisfies C ∨ D. -/
theorem cnf_resolution_soundness {V : Type*} (τ : V → Bool) (v : V)
    (C D : List (CnfLit V))
    (hC : ∃ l ∈ C ++ [CnfLit.pos v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false)
    (hD : ∃ l ∈ D ++ [CnfLit.neg v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false) :
    ∃ l ∈ C ++ D, match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false := by
  cases hv : τ v
  · rcases hC with ⟨l, hl, hsat⟩
    rw [List.mem_append] at hl
    cases hl with
    | inl hlC =>
      refine ⟨l, List.mem_append_left D hlC, hsat⟩
    | inr hlv =>
      simp only [List.mem_singleton] at hlv
      subst hlv
      dsimp at hsat
      rw [hv] at hsat
      contradiction
  · rcases hD with ⟨l, hl, hsat⟩
    rw [List.mem_append] at hl
    cases hl with
    | inl hlD =>
      refine ⟨l, List.mem_append_right C hlD, hsat⟩
    | inr hlv =>
      simp only [List.mem_singleton] at hlv
      subst hlv
      dsimp at hsat
      rw [hv] at hsat
      contradiction

Discuss this result Challenge it