Stefan Dantchev and Søren Riis: On Relativisation and Complexity gap for Resolutionbased proof systems  

In the present paper we prove several generalisations and extensions of the ComplexityGap theorem. 1. It holds for stronger systems, Res* (k). These proof systems are extensions of Treelike Resolution, in which literals are replaced by terms (i.e. conjunctions of literals) of size at most k. 2. For a natural subclass of tautologies, namely the tautologies relativised with respect to a unary predicate, the complexity gap holds even for general (DAGlike) Resolution. The separating modeltheoretic criteria is the same as before. 3. There is no gap for any propositional proof system (including Treelike Resolution) if we enrich the language of SO logic by a builtin order.
