We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments. This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege.

翻译：我们开创了一种新技术，能够证明QBF证明复杂度中多个此前未解决的模拟关系。特别地，我们证明了扩展QBF弗雷格系统可p-模拟子句证明系统，如IR-演算、IRM-演算、长距离Q-消解和合并消解。这些结果通过结合Beyersdorff等人（JACM 2020）将策略提取转化为模拟的技术与新的局部策略提取论证而获得。该方法使得模拟主要通过命题逻辑进行，且最小化使用QBF规则。因此，我们的证明为所模拟系统提供了一种新的、主要基于命题逻辑的解释。我们论证这些结果强化了QBF求解中统一认证的论据，因为现在许多QBF证明系统可归入扩展QBF弗雷格系统之下。