Lower bound techniques for QBF expansion (Q1987510)

The article is well organized, written, and very clear. It proposes a genuine extraction strategy techniques for proving lower bounds in expansion-based QBF proof systems. It shows that the strategy size is an absolute proof-size lower bound in \(\forall\)Exp+Res, and the refined version of that strategy, i.e., the one based on the weight of the extracted strategy is an absolute proof-size lower bound in IR-calc. Besides, the authors prove an exponential IR-calc lower bound for a new class of PCNF family formulas. Finally, it shows that in the absence of propositional hardness formulas separating IR-cal and \(\forall\)Exp+Res must be \(unbounded\) quantifier alternations. Some typos: on page 407 and 415, paragraph 2 on both pages. To conclude, in the proof of Proposition 1, paragraph 1, there is a typo, instead of ``We prove the lemma'' it should be ``We prove the proposition'', and there is another typo in the proof of Proposition 2, paragraph 4, instead of ``We hence prove the lemma'' it should be ``We hence prove the proposition''.