LFCS Seminar

On Relativisation and Complexity gap for Resolution-based proof systems

Stefan Dantchev

Department of Mathematics & Computer Science
University of Leicester

4pm 25 November 2003
Room 2511, JCMB, King's Buildings

---

Abstract

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.

Joint work by Stefan Danchev and Soren Riis.