For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. Apart from a naive system, we study #QBF systems based on the expansion rule of universal variables in QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.

翻译：对于量化布尔公式（QBF），计算获胜策略数量的问题被称为#QBF问题。该问题被认为比类似的#SAT问题更难。近年来，针对QBF和#SAT的重要证明系统已得到研究。通过融合这两个领域的思路，我们表明可以为#QBF设计证明系统。这类证明系统不仅对推进#QBF理论至关重要，还有助于验证和设计更优的#QBF求解器——这一领域仍处于初级阶段。本文探索了用于计算Skolem函数数量的#QBF证明系统。除了一种朴素系统外，我们还研究了基于QBF中全称变量展开规则的#QBF系统。我们观察到这些系统存在固有的结构缺陷，导致其下界受限。作为替代，我们提出了一种名为Q-MICE的#QBF证明系统，该系统包含用于计算和验证#QBF解的正确推理规则，类似于基于行的#SAT证明系统MICE。为展示Q-MICE的效力，我们给出了多种上界结果，例如对MICE而言困难的命题XOR-PAIRS公式的量化版本。由此，我们也实现了Q-MICE与基于展开的#QBF证明系统的分离。