Stefan Dantchev and Søren Riis: On Relativisation and Complexity gap for Resolution-based proof systems | ||||||||||||||||
|
In the present paper we prove several generalisations and extensions of the Complexity-Gap theorem. 1. It holds for stronger systems, Res* (k). These proof systems are extensions of Tree-like 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 (DAG-like) Resolution. The separating model-theoretic criteria is the same as before. 3. There is no gap for any propositional proof system (including Tree-like Resolution) if we enrich the language of SO logic by a built-in order.
|