迈向 QBF 中的统一认证
Towards Uniform Certification in QBF
AI总结：
本文提出一种新技术，将策略提取与局部论证相结合，证明扩展 QBF Frege 可 p-模拟多种子句证明系统，从而支持 QBF 求解中的统一认证。
摘要：
我们开创了一种新技术，使我们能够证明 QBF 证明复杂性中大量先前未解决的模拟关系。具体而言，我们证明了扩展 QBF Frege 系统可以 p-模拟多种子句证明系统，如 IR-Calculus、IRM-Calculus、Long-Distance Q-Resolution 和 Merge Resolution。这些结果是通过采用 Beyersdorff 等人（JACM 2020）提出的将策略提取转化为模拟的技术，并将其与新的局部策略提取论证相结合而获得的。这种方法使得模拟主要在命题逻辑层面进行，仅需极少使用 QBF 规则。因此，我们的证明为被模拟的系统提供了一种新的、以命题逻辑为主的解释。我们认为，这些结果加强了在 QBF 求解中采用统一认证的理由，因为许多 QBF 证明系统现在都可以归入扩展 QBF Frege 的框架之下。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
