Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR20-159 | 9th October 2020 18:47

Relating existing powerful proof systems for QBF

RSS-Feed




TR20-159
Authors: Leroy Chew, Marijn Heule
Publication: 2nd November 2020 11:48
Downloads: 616
Keywords: 


Abstract:

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not have strategy extraction. Because EUR heavily uses resolution paths our technique also brings resolution path dependency and sequent systems closer together.
While we do not recommend G for practical applications this work can potentially show what features are needed for a new QBF checking format stronger than QRAT.



ISSN 1433-8092 | Imprint