论文标题
在QBF中达到统一认证
Towards Uniform Certification in QBF
论文作者
论文摘要
我们开创了一种新技术，使我们能够在QBF证明复杂性中证明许多先前开放的模拟。特别是，我们表明扩展的QBF Frege p-simul in in IR-CALCULUS，IRM-CALCULUS，长距离Q分辨率和合并分辨率等可神经证明系统。这些结果是通过采用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.
