We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

On relativisation and complexity gap for resolution-based proof systems.

Dantchev, S. and Riis, S. (2003) 'On relativisation and complexity gap for resolution-based proof systems.', in Computer science logic : 17th International Workshop CSL 2003, 12th Annual Conference of the EACSL, 8th Kurt Gödel Colloquium, KGC 2003, 25-30 August 2003, Vienna, Austria ; proceedings. Berlin: Springer, pp. 142-154. Lecture notes in computer science. (2803).


We study the proof complexity of Taut, the class of Second-Order Existential (SO∃) 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, 2Ω(n), or polynomial, nO(1), where n is the size of the finite model. Moreover, there is a very simple model-theoretics criteria which separates the two cases: the exponential lower bound holds if and only if Φ holds in some infinite model. In the present paper we prove several generalisations and extensions of the Complexity-Gap theorem. For a natural subclass of Taut, Rel(Taut), there is a gap between polynomial Tree-like Resolution proofs and sub-exponential, 2Ω(nε), general (DAG-like) Resolution proofs, whilst the separating model-theoretic criteria is the same as before. Rel(Taut) is the set of all sentences in Taut, relativised with respect to a unary predicate. The gap for stronger systems, Res∗(k), is between polynomial and exp(Ω(logkkn)) for every k, 1≤ k≤ n. Res∗(k) is an extension of Tree-like Resolution, in which literals are replaced by terms (i.e. conjunctions of literals) of size at most k. The lower bound is tight. There is (as expected) no gap for any propositional proof system (including Tree-like Resolution) if we enrich the language of SO logic by a built-in order.

Item Type:Book chapter
Full text:Full text not available from this repository.
Publisher Web site:
Date accepted:No date available
Date deposited:No date available
Date of first online publication:August 2003
Date first made open access:No date available

Save or Share this output

Look up in GoogleScholar