Resolution

DefinitionResolvent of two clauses#✓fully proved

Let \(x\) be a variable and \(C\), \(D\) clauses. The resolvent of \(C\) and \(D\) on \(x\) is the clause consisting of the literals of \(C\) other than \((x, \mathrm{true})\), in order, followed by the literals of \(D\) other than \((x, \mathrm{false})\), in order.

def resolvent (x : Nat) (C D : CNFClause) : CNFClause :=
  C.filter (· ≠ (x, true)) ++ D.filter (· ≠ (x, false))

Uses 1 · Used by 11

Statement usesCNF clause

Used byResolution refutations give contradictory cycles · Correctness of the Davis-Putnam procedure · Davis-Putnam elimination of a variable · Completeness of a Davis-Putnam step · Resolvents do not mention the resolved variable · Soundness of a Davis-Putnam step · Lifting lemma · Resolution derivability · Refutation completeness · Soundness of resolution · Resolution rule soundness

TheoremResolution rule soundness#✓fully proved

Let \(x\) be a variable and \(C\), \(D\) clauses. Every assignment that satisfies both \(C\) and \(D\) satisfies the resolvent of \(C\) and \(D\) on \(x\).

theorem satisfies_resolvent {assignment : Nat → Bool} {x : Nat} {C D : CNFClause}
    (hC : C.Satisfies assignment) (hD : D.Satisfies assignment) :
    (resolvent x C D).Satisfies assignment

Uses 4 · Used by 2

Statement usesCNF clause · Satisfaction of a clause · Resolvent of two clauses

Proof usesSatisfaction of a literal

Used bySoundness of a Davis-Putnam step · Soundness of resolution

InductiveResolution derivability#✓fully proved

Given a CNF formula \(\varphi\), the clauses derivable from \(\varphi\) by resolution form the smallest set \(S\) of clauses that contains every clause of \(\varphi\) and, for every variable \(x\) and all clauses \(C, D \in S\) such that \(C\) contains the literal \((x, \mathrm{true})\) and \(D\) contains the literal \((x, \mathrm{false})\), contains the resolvent of \(C\) and \(D\) on \(x\).

inductive ResolutionDerivable (φ : CNF) : CNFClause → Prop
  /-- Every clause of the formula is derivable. -/
  | ax {C : CNFClause} : C ∈ φ → ResolutionDerivable φ C
  /-- Resolve a clause containing `(x, true)` with one containing `(x, false)`. -/
  | resolve {C D : CNFClause} (x : Nat) :
      ResolutionDerivable φ C → ResolutionDerivable φ D → (x, true) ∈ C → (x, false) ∈ D →
      ResolutionDerivable φ (CNFClause.resolvent x C D)

Uses 3 · Used by 6

Statement usesCNF formula · CNF clause · Resolvent of two clauses

Used byResolution refutations give contradictory cycles · Lifting lemma · Refutable formulas are unsatisfiable · Soundness and refutation completeness · Refutation completeness · Soundness of resolution

10 fully proved

Soundness

TheoremSoundness of resolution#✓fully proved

Let \(\varphi\) be a CNF formula. Every clause derivable by resolution from \(\varphi\) is satisfied by every assignment that satisfies \(\varphi\).

theorem ResolutionDerivable.satisfies {φ : CNF} {C : CNFClause} {assignment : Nat → Bool}
    (h : φ.ResolutionDerivable C) (hφ : φ.Satisfies assignment) : C.Satisfies assignment

Uses 7 · Used by 1

Statement usesCNF formula · Resolution derivability · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

Proof usesResolvent of two clauses · Resolution rule soundness

Used byRefutable formulas are unsatisfiable

TheoremRefutable formulas are unsatisfiable#✓fully proved

If the empty clause is derivable by resolution from a CNF formula \(\varphi\), then \(\varphi\) is not satisfiable.

theorem not_cnfSat_of_resolutionDerivable_nil {φ : CNF} (h : φ.ResolutionDerivable []) :
    ¬ CNFSat φ

Uses 8 · Used by 1

Statement usesCNF formula · Resolution derivability · Satisfiability of a CNF formula

Proof usesSoundness of resolution · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Satisfiability means having a satisfying assignment

Used bySoundness and refutation completeness

Completeness

TheoremClauses of a restricted formula#✓fully proved

Let \(\varphi\) be a CNF formula and \(\ell\) a literal. A clause \(C\) belongs to the restriction of \(\varphi\) by \(\ell\) if and only if there is a clause \(C_0\) of \(\varphi\) that does not contain \(\ell\) such that \(C\) is the restriction of \(C_0\) by \(\ell\).

theorem mem_restrict_iff {literal : Nat × Bool} {φ : CNF} {C : CNFClause} :
    C ∈ φ.restrict literal ↔ ∃ C₀ ∈ φ, literal ∉ C₀ ∧ C = C₀.restrict literal

Uses 4 · Used by 1

Statement usesCNF formula · Restriction of a CNF formula by a literal · CNF clause · Restriction of a clause by a literal

Used byLifting lemma

TheoremLifting lemma#✓fully proved

Let \(\varphi\) be a CNF formula, \(x\) a variable and \(b\) a Boolean value. If a clause \(D\) is derivable by resolution from the restriction of \(\varphi\) by the literal \((x, b)\), then some clause \(D_0\) is derivable by resolution from \(\varphi\) such that every literal of \(D_0\) is either a literal of \(D\) or the complementary literal \((x, \lnot b)\).

theorem ResolutionDerivable.lift_restrict {φ : CNF} {x : Nat} {b : Bool} {D : CNFClause}
    (h : (φ.restrict (x, b)).ResolutionDerivable D) :
    ∃ D₀, φ.ResolutionDerivable D₀ ∧ ∀ l ∈ D₀, l ∈ D ∨ l = (x, !b)

Uses 7 · Used by 1

Statement usesCNF formula · Resolution derivability · Restriction of a CNF formula by a literal · CNF clause

Proof usesClauses of a restricted formula · Resolvent of two clauses · Restriction of a clause by a literal

Used byRefutation completeness

TheoremUnsatisfiable formulas without variables contain the empty clause#✓fully proved

If a CNF formula \(\varphi\) has no variables and is not satisfiable, then the empty clause is one of the clauses of \(\varphi\).

theorem nil_mem_of_vars_eq_empty {φ : CNF} (hvars : φ.vars = ∅) (hφ : ¬ CNFSat φ) :
    [] ∈ φ

Uses 5 · Used by 2

Statement usesCNF formula · Variables of a CNF formula · CNF clause · Satisfiability of a CNF formula

Proof usesVariables of a clause

Used byCorrectness of the Davis-Putnam procedure · Refutation completeness

TheoremRefutation completeness#✓fully proved

Refutation completeness of resolution: every unsatisfiable CNF formula has a resolution derivation of the empty clause.

theorem resolutionDerivable_nil_of_not_cnfSat {φ : CNF} (hφ : ¬ CNFSat φ) :
    φ.ResolutionDerivable []

Uses 11 · Used by 2

Statement usesCNF formula · Resolution derivability · Satisfiability of a CNF formula

Proof usesLifting lemma · Restriction reduces the number of variables · Unsatisfiable formulas without variables contain the empty clause · Restriction of a CNF formula by a literal · Splitting on a variable · Variables of a CNF formula · CNF clause · Resolvent of two clauses

Used by2-SAT characterization · Soundness and refutation completeness

TheoremSoundness and refutation completeness#✓fully proved

A CNF formula has a resolution refutation iff it is unsatisfiable.

theorem resolutionDerivable_nil_iff_not_cnfSat {φ : CNF} :
    φ.ResolutionDerivable [] ↔ ¬ CNFSat φ

Uses 5

Statement usesCNF formula · Resolution derivability · Satisfiability of a CNF formula

Proof usesRefutable formulas are unsatisfiable · Refutation completeness

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.