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).

## 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.

Item Type: | Book chapter |
---|---|

Full text: | Full text not available from this repository. |

Publisher Web site: | http://dx.doi.org/10.1007/978-3-540-45220-1_14 |

Record Created: | 30 Oct 2008 |

Last Modified: | 09 Oct 2014 12:39 |

Social bookmarking: | Export: EndNote, Zotero | BibTex |

Look up in GoogleScholar | Find in a UK Library |