The Community for Technology Leaders
RSS Icon
Subscribe
San Jose, California USA
June 8, 2011 to June 11, 2011
ISBN: 978-0-7695-4411-3
pp: 93-103
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 Erdos and Mills.
INDEX TERMS
proof complexity, bounded-depth frege, resolution, ramsey
CITATION
Lorenzo Carlucci, Nicola Galesi, Massimo Lauria, "Paris-Harrington Tautologies", CCC, 2011, 2012 IEEE 27th Conference on Computational Complexity, 2012 IEEE 27th Conference on Computational Complexity 2011, pp. 93-103, doi:10.1109/CCC.2011.17
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool