Lax Lean Archive

PSPACE-hardness of the positive CNF game

Lax689614.PositiveCNFHardness · concepts/Lax689614/PositiveCNFHardness.lean · lax-689614

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Schaefer's theorem: determining whether True wins the positive CNF game is PSPACE-hard under polynomial-time many-one reductions.

    Concept map
    12 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax689614.Encoding
    2import Lax689614.PSPACE
    3
    4/-!
    5---
    6title: PSPACE-hardness of the positive CNF game
    7type: theorem
    8---
    9Schaefer's theorem: determining whether True wins the positive CNF game
    10is PSPACE-hard under polynomial-time many-one reductions.
    11
    12# References
    13Thomas J. Schaefer, *On the complexity of some two-person
    14perfect-information games*, JCSS 16(2), 185–225 (1978).
    15-/
    16
    17namespace Lax689614.PositiveCNFHardness
    18
    19axiom hard : PSPACE.Hard Encoding.positiveCNF
    20
    21end Lax689614.PositiveCNFHardness
    22
    Show Proof

    References

    Thomas J. Schaefer, On the complexity of some two-person perfect-information games, JCSS 16(2), 185–225 (1978).

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…