Header menu link for other important links
X
A game characterisation of tree-like q-resolution size
O. Beyersdorff, L. Chew,
Published in Springer Verlag
2015
Volume: 8977
   
Pages: 486 - 498
Abstract
We provide a characterisation for the size of proofs in treelike Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution [10]. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF proof systems. We confirm our technique with two previously known hard examples. In particular, we give a proof of the hardness of the formulas of Kleine Büning et al. [20] for tree-like Q-Resolution. © Springer International Publishing Switzerland 2015.