Computer Science Logic and 8th Kurt Gödel Colloquium
Stefan Dantchev and Søren Riis: On Relativisation and Complexity gap for Resolution-based proof systems
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
We study the proof complexity of the Second-Order Existential logical sentences which fail in all finite models. The Complexity-Gap theorem for Tree-like Resolution says that the shortest Tree-like Resolution refutation of any such sentence is either fully exponential or polynomial in the size of the model. Moreover, there is a very simple model-theoretics criteria which separates the two cases: the exponential lower bound holds if and only if the sentence holds in some infinite model.

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.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian