Number of the records: 1
A note on propositional proof complexity of some Ramsey-type statements
- 1.
SYSNO ASEP 0369652 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title A note on propositional proof complexity of some Ramsey-type statements Author(s) Krajíček, Jan (MU-W) SAI, ORCID Source Title Archive for Mathematical Logic. - : Springer - ISSN 0933-5846
Roč. 50, 1-2 (2011), s. 245-255Number of pages 11 s. Language eng - English Country DE - Germany Keywords proof complexity ; Ramsey theorem ; resolution Subject RIV BA - General Mathematics R&D Projects IAA100190902 GA AV ČR - Academy of Sciences of the Czech Republic (AV ČR) LC505 GA MŠMT - Ministry of Education, Youth and Sports (MEYS) CEZ AV0Z10190503 - MU-W (2005-2011) UT WOS 000286668400014 EID SCOPUS 79251623828 DOI 10.1007/s00153-010-0212-9 Annotation A Ramsey statement denoted n -> (k)(2)(2) says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into a valid DNF formulaRAM(n, k) of size O(n(k)) and with terms of size ((k)(2)). Let r(k) be the minimal n for which the statement holds. We prove that RAM(r(k), k) requires exponential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll [15]. As a consequence of Pudlak's work in bounded arithmetic [19] it is known that there are quasi-polynomial size constant depth Frege proofs of RAM(4(k), k), but the proof complexity of these formulas in resolution R or in its extension R(log) is unknown. We define two relativizations of the Ramsey statement that still have quasi-polynomial size constant depth Frege proofs but for which we establish exponential lower bound for R. Workplace Mathematical Institute Contact Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Year of Publishing 2012
Number of the records: 1