Semi-Algebraic Proof Systems for QBF

TL;DR

This paper introduces semi-algebraic proof systems for QBF, adapting techniques from propositional proof complexity and QBF literature to establish new lower bounds and separations.

Contribution

It develops novel semi-algebraic proof systems for QBF and applies advanced techniques to derive strong lower bounds and system separations.

Findings

Established new QBF lower bounds

Demonstrated separations between proof systems

Transferred techniques from propositional proof complexity

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.