| Summary: | 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.
|
|---|