# Gap theorems in Proof Complexity

**Speaker:**Dr Barnaby Martin, School of Science and Technology, Middlesex University, London.**Date:**Wednesday, 9 October 2013 from 16:30 to 17:30**Location:**Room 160, Birkbeck Main Building

The origins of Proof Complexity lie largely in the program of Cook and Reckow, who aimed to separate P and NP (actually, coNP and NP) by proving that no propositional proof system is polynomially bounded. Having failed to obtain such a general result, students of Proof Complexity have instead focused on proving that stronger and stronger proof systems are not polynomially bounded. Such lower bounds are known for systems such as Resolution and Bounded-depth Frege.

Resolution is in fact a refutation system in which one proves that a propositional formula in CNF is a contradiction. A classic result from the area concerns the tree-like restriction of Resolution. Riis proved that contradictions that uniformly encode a first-order principle without finite models over a universe of size n either 1.) have refutations of size n^{O(1)} or 2.) require size 2^{en} for some positive e. The latter case prevails precisely when the first-order principle has an infinite model.

We will give an introduction to Riis's celebrated result and go on to consider more recent gap theorems in refutation systems based on Integer Linear Programming, such as Lovasz-Schrijver and Sherali-Adams.