English

Semi-Algebraic Proof Systems for QBF

Logic in Computer Science 2025-11-12 v1 Computational Complexity Logic

Abstract

We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.

Cite

@article{arxiv.2511.08050,
  title  = {Semi-Algebraic Proof Systems for QBF},
  author = {Olaf Beyersdorff and Ilario Bonacina and Kaspar Kasche and Meena Mahajan and Luc Nicolas Spachmann},
  journal= {arXiv preprint arXiv:2511.08050},
  year   = {2025}
}
R2 v1 2026-07-01T07:31:41.272Z