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消解和合并消解。这些结果通过融合贝耶斯多夫等人（JACM 2020）将策略提取转化为模拟的技术与新的局部策略提取论证而获得。该方法使得模拟主要基于命题逻辑实现，仅最小程度使用QBF规则。因此，我们的证明为被模拟系统提供了全新的、主要基于命题逻辑的解读。我们认为，这些结果强化了QBF求解中统一验证的依据——目前众多QBF证明系统已可归入扩展QBF弗雷格系统框架之下。