Characterising tree-like Frege proofs for QBF

We examine the tree-like versions of QBF Frege and extended Frege systems. While in the propositional setting, tree-like and dag-like Frege are equivalent, we show that this is not the case for QBF Frege, where tree-like systems are exponentially weaker. This applies to the version of QBF Frege wher...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2019-10, Vol.268, p.104429, Article 104429
Main Authors: Beyersdorff, Olaf, Hinde, Luke
Format: Article
Language:English
Subjects:
Frege systems
Lower bounds
Proof complexity
QBF
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We examine the tree-like versions of QBF Frege and extended Frege systems. While in the propositional setting, tree-like and dag-like Frege are equivalent, we show that this is not the case for QBF Frege, where tree-like systems are exponentially weaker. This applies to the version of QBF Frege where the universal reduction rule substitutes universal variables by 0/1 constants. To show lower bounds for tree-like QBF Frege we devise a general technique that provides lower bounds for all tree-like QBF systems of the form P+∀red, where P is a propositional system. The lower bound is based on the semantic measure of strategy size corresponding to the size of countermodels for false QBFs. We also obtain a full characterisation of hardness for tree-like QBF Frege. Lower bounds for this system either arise from a lower bound to propositional Frege, from a circuit lower bound, or from a lower bound to strategy size.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2019.05.002