CnfLit

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

Statement

inductive CnfLit (V : Type*)

Verified

06 Sep 2026

Axioms

none listed

Used by 6

• cnf_resolution_soundnessSoundness of the resolution rule: for any truth assignment `τ : V → Bool`, variable `v : V`, and clauses `C, D : List (CnfLit V)`, if…
• cnf_satisfiable_append_sum_iffLet f be a CNF formula over a variable type V and g a CNF formula over a variable type W. Replace every literal of f by the literal of the…
• cnf_satisfiable_subsetIf every clause of a CNF formula `f1` is contained in a CNF formula `f2` (that is, `f1 ⊆ f2`), and `f2` is satisfiable (`CnfSatisfiable…
• cnf_single_clause_satisfiable_iffA CNF formula consisting of a single clause `c`, namely `[c]`, is satisfiable (`CnfSatisfiable [c]`) if and only if the clause `c` is…
• cnf_satisfiable_of_appendIf the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable…
• CnfSatisfiableA CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains…

Lean source view module on GitHub

/-- A literal over variable type `V`, either a positive or negative occurrence of a variable. -/
inductive CnfLit (V : Type*) | pos (v : V) : CnfLit V
  | neg (v : V) : CnfLit V