Header menu link for other important links
X
A game characterisation of tree-like Q-Resolution size
O. Beyersdorff, L. Chew,
Published in Academic Press Inc.
2019
Volume: 104
   
Pages: 82 - 101
Abstract
We provide a characterisation for the size of proofs in tree-like Q-Resolution and tree-like QU-Resolution by a Prover–Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives one of the first successful transfers of one of the lower bound techniques for classical proof systems to QBF proof systems. We apply our technique to show the hardness of three classes of formulas for tree-like Q-Resolution. In particular, we give a proof of the hardness of the parity formulas from Beyersdorff et al. (2015) [10] for tree-like Q-Resolution and of the formulas of Kleine Büning et al. (1995) [29] for tree-like QU-Resolution. © 2017 The Authors
About the journal
JournalJournal of Computer and System Sciences
PublisherAcademic Press Inc.
ISSN00220000