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 Frege系统在多项式时间内模拟子句证明系统，包括IR-演算、IRM-演算、长距离Q-消解和合并消解。这些结果通过结合Beyersdorff等人（JACM 2020）将策略提取转化为模拟的技术与新的局部策略提取论证而获得。该方法使得模拟主要在命题逻辑中实现，仅需最小限度地使用QBF规则。因此，我们的证明为被模拟系统提供了新的、主要基于命题逻辑的解释。我们认为这些结果强化了QBF求解中统一认证的合理性，因为当前众多QBF证明系统已可归入扩展QBF Frege框架之下。