DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-12

How 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.

Quantified Boolean formulas and the language TQBF

Definition

A quantified Boolean formula is a formula of the form

$Q_{1} x_{1} Q_{2} x_{2} \dots Q_{m} x_{m} ψ (x_{1}, \dots, x_{m}),$

where each $Q_{i}$ is either $\exists$ or $\forall$ , and $ψ$ is a quantifier-free Boolean formula built from the variables $x_{1}, \dots, x_{m}$ , the constants $0, 1$ , and the connectives $\neg, \land, \lor$ .

Such a formula is true when its usual recursive Boolean semantics evaluates to true. The language TQBF consists of all true quantified Boolean formulas under any fixed effective encoding of these strings.

Remarks

The page uses prenex form so that the quantifier prefix can be read from left to right.
TQBF is a decision problem about truth, not satisfiability of only the quantifier-free matrix.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach (standard reference, not scraped)
Eric Blais, Models of Computation, 17. Space Complexity (standard reference, not scraped)