一句话：提出策略提取模拟技术，证明扩展 QBF Frege 可 p-模拟多种子句 QBF 证明系统，支持 QBF 求解统一认证。
本文研究 QBF 证明复杂度中的模拟问题，并面向 QBF 求解的认证需求。作者提出一种新技术：将 Beyersdorff 等人把策略提取转化为模拟的方法，与新的局部策略提取论证相结合。利用该技术，他们证明扩展 QBF Frege 可 p-模拟多种子句证明系统，包括 IR-Calculus、IRM-Calculus、Long-Distance Q-Resolution 和 Merge Resolution。这些模拟主要在命题逻辑中完成，仅最小程度地使用 QBF 规则，从而为被模拟系统提供了新的、大体命题化的解释。作者认为，大量 QBF 证明系统由此归入扩展 QBF Frege 之下，强化了 QBF 求解中统一认证的论据。
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.