Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR10-153 | 27th September 2011 19:09

Paris-Harrington tautologies

RSS-Feed




Revision #2
Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria
Accepted on: 27th September 2011 19:09
Downloads: 2789
Keywords: 


Abstract:

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 to TR10-153 | 27th April 2011 07:51

Paris-Harrington tautologies





Revision #1
Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria
Accepted on: 27th April 2011 07:51
Downloads: 2603
Keywords: 


Abstract:

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


Paper:

TR10-153 | 7th October 2010 12:12

Paris-Harrington tautologies





TR10-153
Authors: Lorenzo Carlucci, Nicola Galesi, Massimo Lauria
Publication: 7th October 2010 15:48
Downloads: 4213
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint