Olaf Beyersdorff, Judith Clymo, Stefan Dantchev, Barnaby Martin

We give an analogue of the Riis Complexity Gap Theorem for Quanti fied Boolean Formulas (QBFs). Every fi rst-order sentence $\phi$ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like Q-Resolution are either of polynomial size (if $\phi$ has no models) or at least ... more >>>