Revision #2 Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

Accepted on: 27th September 2011 19:09

Downloads: 2829

Keywords:

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

Revision #1 Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

Accepted on: 27th April 2011 07:51

Downloads: 2613

Keywords:

We study the proof complexity of Paris-Harringtonâ€™s Large Ramsey Theorem for bi-colorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in Res(2). We show that under such assumption, there is no refutation of the Paris-Harrington formulas of size quasi-polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by adapting some constructions due to Erd?s and Mills

TR10-153 Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

Publication: 7th October 2010 15:48

Downloads: 4259

Keywords:

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.