Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Boolean formulas, conjunctive normal form, and the satisfiability language SAT
Definition
A Boolean formula is built from variables, the constants , and the connectives in the usual recursive way. A formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, where each clause is a disjunction of literals and a literal is either a variable or the negation of a variable.
The language consists of the encodings of Boolean formulas that admit a truth assignment making them true.
Remarks
-
A -CNF formula is a CNF formula whose clauses have at most three literals.
-
On this page, formulas are encoded by any fixed reasonable binary syntax; completeness statements are invariant under that choice up to polynomial-time translation.
Used by
- Tseitin extension variables for subformulas Definition
- FALSE: distributing an arbitrary formula into CNF always has polynomial size False statement
- A three-CNF formula as a fixed-alphabet binary constraint graph Lemma
- The Cook-Levin formula is satisfiable if and only if an accepting bounded tableau exists Lemma
- The exactly-one-symbol constraints have polynomial size Lemma
- The start, accept, and transition constraints have polynomial size Lemma
- The Tseitin transformation has linear size and preserves satisfiability Lemma
- SAT lies in NP Proposition
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- MIT 18.404J / 6.840J Theory of Computation, Lecture Notes (standard reference, not scraped)
- Stephen A. Cook, The Complexity of Theorem-Proving Procedures (standard reference, not scraped)