On relativisation and complexity gap for resolution-based proof systems

Dantchev, Stefan; Riis, Soren

Abstract

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.

Citation

Dantchev, S., & Riis, S. (2003, August). On relativisation and complexity gap for resolution-based proof systems. Presented at 12th Annual Conference of the EACSL Computer Science Logic., Vienna, Austria

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 12th Annual Conference of the EACSL Computer Science Logic.
• Start Date: Aug 25, 2003
• End Date: Aug 30, 2003
• Publication Date: 2003-08
• Deposit Date: Oct 30, 2008
• Print ISSN: 0302-9743
• Pages: 142-154
• Series Title: Lecture notes in computer science
• Series Number: 2803
• Series ISSN: 0302-9743
• Book Title: 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
• DOI: https://doi.org/10.1007/978-3-540-45220-1_14
• Public URL: https://durham-repository.worktribe.com/output/1695105
• Additional Information: 25-30 Aug 2003.