QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful in line-based proof systems, is not refutationally complete for static proof systems.

Nullstellensatz (NS, [Beame et al. FOCS.'1994]) is a well known static propositional proof system, inspired by Hilbert's theorem [Hilbert Math. Ann.'1893] of the same name. It falls into the category of algebraic proof systems such as the Polynomial Calculus [Book, Krají?ek Cam. Uni.'2019, p.162] or the Ideal Proof System (IPS,[Grochow et al. J. ACM.'2018]). In this paper, we initiate the study of the NS proof system for QBFs using the existing expansion ($\forall$Exp) framework and a new "$\forall$Strat" framework. We introduce four new static QBF refutation systems: $\forall$Exp+NS, $\forall$Exp+NS', $\forall$Strat+NS and $\forall$Strat+NS', which use NS and a more powerful version of NS (NS') with twin variable encoding that allows it to simulate tree-like resolution without an exponential blowup.

We explore relationships among the proposed systems and analyse their proof sizes for a few well-known hard QBF-families. We find that $\forall$Exp+NS' and $\forall$Strat+NS' are incomparable. This result is in line with the incomparability result between ?Exp+Res and Q-Res [Beyersdorff et al. STACS.'2015].