{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:44:14Z","timestamp":1743151454626,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319202969"},{"type":"electronic","value":"9783319202976"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-20297-6_1","type":"book-chapter","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T01:55:05Z","timestamp":1434938105000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Propositional Proofs in Frege and Extended Frege Systems (Abstract)"],"prefix":"10.1007","author":[{"given":"Sam","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,23]]},"reference":[{"key":"1_CR1","unstructured":"Aisenberg, J., Bonet, M.L., Buss, S.: Quasi-polynomial size Frege proofs of Frankl\u2019s theorem on the trace of finite sets. J. Symbolic Log. (to appear)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Aisenberg, J., Bonet, M.L., Buss, S., Cr\u00e3ciun, A., Istrate, G.: Short proofs of the Kneser-Lov\u00e1sz principle. In: Proceedings of 42th International Colloquium on Automata, Languages, and Programming (ICALP 2015) (2015) (to appear)","DOI":"10.1007\/978-3-662-47666-6_4"},{"key":"1_CR3","first-page":"1","volume-title":"Proof Complexity and Feasible Arithmetics","author":"J Avigad","year":"1997","unstructured":"Avigad, J.: Plausibly hard combinatorial tautologies. In: Beame, P., Buss, S.R. (eds.) Proof Complexity and Feasible Arithmetics, pp. 1\u201312. American Mathematical Society, Rutgers (1997)"},{"key":"1_CR4","series-title":"IAS\/Park City Mathematical Series","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1090\/pcms\/010\/07","volume-title":"Computational Complexity Theory","author":"P Beame","year":"2004","unstructured":"Beame, P.: Proof complexity. In: Rudich, S., Wigderson, A. (eds.) Computational Complexity Theory. IAS\/Park City Mathematical Series, vol. 10, pp. 199\u2013246. American Mathematical Society, Princeton (2004)"},{"key":"1_CR5","first-page":"42","volume-title":"Current Trends in Theoretical Computer Science Entering the 21st Century","author":"P Beame","year":"2001","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present and future. In: Paun, G., Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science Entering the 21st Century, pp. 42\u201370. World Scientific Publishing Co. Ltd, Singapore (2001). Earlier version appeared in Computational Complexity Column, Bulletin of the EATCS (2000)"},{"issue":"1","key":"1_CR6","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/2559950","volume":"15","author":"A Beckmann","year":"2014","unstructured":"Beckmann, A., Buss, S.R.: Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Trans. Comput. Logic 15(1), 35 (2014)","journal-title":"ACM Trans. Comput. Logic"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-1-4612-2566-9_3","volume-title":"Feasible Mathematics II","author":"ML Bonet","year":"1995","unstructured":"Bonet, M.L., Buss, S.R., Pitassi, T.: Are there hard examples for Frege systems? In: Clote, P., Remmel, J. (eds.) Feasible Mathematics II, pp. 30\u201356. Birkh\u00e4user, Boston (1995)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.tcs.2015.02.005","volume":"576","author":"S Buss","year":"2015","unstructured":"Buss, S.: Quasipolynomial size proofs of the propositional pigeonhole principle. Theor. Comput. Sci. 576, 77\u201384 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR9","unstructured":"Buss, S.R.: Bounded Arithmetic. Ph.D. thesis, Bibliopolis, Princeton University (revision of 1985) (1986)"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"SR Buss","year":"1987","unstructured":"Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symbolic Logic 52, 916\u2013927 (1987)","journal-title":"J. Symbolic Logic"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0168-0072(91)90036-L","volume":"52","author":"SR Buss","year":"1991","unstructured":"Buss, S.R.: Propositional consistency proofs. Ann. Pure Appl. Logic 52, 3\u201329 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-58622-4_5","volume-title":"Computational Logic","author":"SR Buss","year":"1999","unstructured":"Buss, S.R.: Propositional proof complexity: an introduction. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic, pp. 127\u2013178. Springer-Verlag, Berlin (1999)"},{"issue":"9","key":"1_CR13","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.1016\/j.apal.2012.01.015","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and proof search. Ann. Pure Appl. Logic 163(9), 1163\u20131182 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Cook, S.A., Reckhow, R.A.: On the lengths of proofs in the propositional calculus, preliminary version. In: Proceedings of the Sixth Annual ACM Symposium on the Theory of Computing, pp. 135\u2013148 (1974)","DOI":"10.1145\/800119.803893"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44, 36\u201350 (1979)","journal-title":"J. Symbolic Logic"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1137\/130917788","volume":"44","author":"P Hrube\u0161","year":"2015","unstructured":"Hrube\u0161, P., Tzameret, I.: Short proofs for determinant identities. SIAM J. Comput. 44(2), 340\u2013383 (2015)","journal-title":"SIAM J. Comput."},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/978-3-319-09284-3_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Istrate","year":"2014","unstructured":"Istrate, G., Cr\u00e3ciun, A.: Proof complexity and the Kneser-Lov\u00e1sz theorem. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 138\u2013153. Springer, Heidelberg (2014)"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2003.12.003","volume":"124","author":"E Je\u0159\u00e1bek","year":"2004","unstructured":"Je\u0159\u00e1bek, E.: Dual weak pigeonhole principle, boolean complexity, and derandomization. Ann. Pure Appl. Logic 124, 1\u201337 (2004)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"1_CR19","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/j.apal.2010.12.002","volume":"162","author":"LA Ko\u0142odziejczyk","year":"2011","unstructured":"Ko\u0142odziejczyk, L.A., Nguyen, P., Thapen, N.: The provably total NP search problems of weak second-order bounded arithmetic. Ann. Pure Appl. Logic 162(2), 419\u2013446 (2011)","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Arithmetic: Propositional Calculus and Complexity Theory","author":"J Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic: Propositional Calculus and Complexity Theory. Cambridge University Press, New York (1995)"},{"issue":"3","key":"1_CR21","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0097-3165(78)90022-5","volume":"25","author":"L Lov\u00e1sz","year":"1978","unstructured":"Lov\u00e1sz, L.: Kneser\u2019s conjecture, chromatic number, and homotopy. J. Comb. Theor. A 25(3), 319\u2013324 (1978)","journal-title":"J. Comb. Theor. A"},{"issue":"1","key":"1_CR22","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s00493-004-0011-1","volume":"24","author":"J Matou\u0161ek","year":"2004","unstructured":"Matou\u0161ek, J.: A combinatorial proof of Kneser\u2019s conjecture. Combinatorica 24(1), 163\u2013170 (2004)","journal-title":"Combinatorica"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-79709-8_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"P Pudl\u00e1k","year":"2008","unstructured":"Pudl\u00e1k, P.: Twelve problems in proof complexity. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) Computer Science \u2013 Theory and Applications. LNCS, vol. 5010, pp. 13\u201327. Springer, Heidelberg (2008)"},{"key":"1_CR24","unstructured":"Reckhow, R.A.: On the lengths of proofs in the propositional calculus. Ph.D. thesis, Department of Computer Science, University of Toronto, Technical report #87 (1976)"},{"issue":"4","key":"1_CR25","doi-asserted-by":"publisher","first-page":"417","DOI":"10.2178\/bsl\/1203350879","volume":"13","author":"N Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bull. Symbolic Logic 13(4), 417\u2013481 (2007)","journal-title":"Bull. Symbolic Logic"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Tsejtin, G.S.: On the complexity of derivation in propositional logic. Studies in Constructive Mathematics and Mathematical Logic 2, pp. 115\u2013125 (1968). Reprinted in J. Siekmann and G. Wrightson, Automation of Reasoning, vol. 2, Springer-Verlag, pp. 466\u2013483 (1983)","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Computer Science -- Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20297-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:49:45Z","timestamp":1676944185000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20297-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319202969","9783319202976"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20297-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}