{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:23:38Z","timestamp":1725557018676},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642135613"},{"type":"electronic","value":"9783642135620"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13562-0_3","type":"book-chapter","created":{"date-parts":[[2010,5,31]],"date-time":"2010-05-31T05:08:30Z","timestamp":1275282510000},"page":"15-27","source":"Crossref","is-referenced-by-count":1,"title":["Proof Complexity of Non-classical Logics"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02579196","volume":"7","author":"N. Alon","year":"1987","unstructured":"Alon, N., Boppana, R.B.: The monotone circuit complexity of boolean functions. Combinatorica\u00a07(1), 1\u201322 (1987)","journal-title":"Combinatorica"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1137\/S0097539701389944","volume":"34","author":"M. Alekhnovich","year":"2004","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Pseudorandom generators in propositional proof complexity. SIAM Journal on Computing\u00a034(1), 67\u201388 (2004)","journal-title":"SIAM Journal on Computing"},{"issue":"4","key":"3_CR3","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/BF01302964","volume":"14","author":"M. Ajtai","year":"1994","unstructured":"Ajtai, M.: The complexity of the pigeonhole-principle. Combinatorica\u00a014(4), 417\u2013433 (1994)","journal-title":"Combinatorica"},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/978-1-4612-2566-9_3","volume-title":"Feasible Mathematics II","author":"M.L. 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, Basel (1995)"},{"key":"3_CR5","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol.\u00a053. Cambridge University Press, Cambridge (2001)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P.W., Impagliazzo, R., Kraj\u00ed\u010dek, J., Pitassi, T., Pudl\u00e1k, P., Woods, A.: Exponential lower bounds for the pigeonhole principle. In: Proc. 24th ACM Symposium on Theory of Computing, pp. 200\u2013220 (1992)","DOI":"10.1145\/129712.129733"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1112\/plms\/s3-73.1.1","volume":"73","author":"P.W. Beame","year":"1996","unstructured":"Beame, P.W., Impagliazzo, R., Kraj\u00ed\u010dek, J., Pitassi, T., Pudl\u00e1k, P.: Lower bounds on Hilbert\u2019s Nullstellensatz and propositional proofs. Proc. London Mathematical Society\u00a073(3), 1\u201326 (1996)","journal-title":"Proc. London Mathematical Society"},{"issue":"1-3","key":"3_CR8","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0168-0072(99)00002-0","volume":"99","author":"S.R. Buss","year":"1999","unstructured":"Buss, S.R., Mints, G.: The complexity of the disjunction and existential properties in intuitionistic logic. Annals of Pure and Applied Logic\u00a099(1-3), 93\u2013104 (1999)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. 13th International Conference on Theory and Applications of Satisfiability Testing","author":"O. Beyersdorff","year":"2010","unstructured":"Beyersdorff, O., Meier, A., M\u00fcller, S., Thomas, M., Vollmer, H.: Proof complexity of propositional default logic. In: Proc. 13th International Conference on Theory and Applications of Satisfiability Testing. LNCS. Springer, Heidelberg (2010)"},{"issue":"2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/505372.505374","volume":"3","author":"P.A. Bonatti","year":"2002","unstructured":"Bonatti, P.A., Olivetti, N.: Sequent calculi for propositional nonmonotonic logics. ACM Transactions on Computational Logic\u00a03(2), 226\u2013278 (2002)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1-2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0168-0072(01)00040-9","volume":"109","author":"S.R. Buss","year":"2001","unstructured":"Buss, S.R., Pudl\u00e1k, P.: On the computational content of intuitionistic propositional proofs. Annals of Pure and Applied Logic\u00a0109(1-2), 49\u201363 (2001)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01200117","volume":"3","author":"P.W. Beame","year":"1993","unstructured":"Beame, P.W., Pitassi, T., Impagliazzo, R.: Exponential lower bounds for the pigeonhole principle. Computational Complexity\u00a03(2), 97\u2013140 (1993)","journal-title":"Computational Complexity"},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"708","DOI":"10.2307\/2275569","volume":"62","author":"M.L. Bonet","year":"1997","unstructured":"Bonet, M.L., Pitassi, T., Raz, R.: Lower bounds for cutting planes proofs with small coefficients. The Journal of Symbolic Logic\u00a062(3), 708\u2013728 (1997)","journal-title":"The Journal of Symbolic Logic"},{"issue":"6","key":"3_CR14","doi-asserted-by":"publisher","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M.L. Bonet","year":"2000","unstructured":"Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems. SIAM Journal on Computing\u00a029(6), 1939\u20131967 (2000)","journal-title":"SIAM Journal on Computing"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E. Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the ACM\u00a048(2), 149\u2013169 (2001)","journal-title":"Journal of the ACM"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. 28th ACM Symposium on Theory of Computing, pp. 174\u2013183 (1996)","DOI":"10.1145\/237814.237860"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S.A. Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic\u00a044(1), 36\u201350 (1979)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2\/3&4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0743-1066(93)90029-G","volume":"17","author":"M. Cadoli","year":"1993","unstructured":"Cadoli, M., Schaerf, M.: A survey of complexity results for nonmonotonic logics. Journal of Logic Programming\u00a017(2\/3&4), 127\u2013160 (1993)","journal-title":"Journal of Logic Programming"},{"key":"3_CR19","unstructured":"Dowd, M.: Model-theoretic aspects of P\u2260NP (1985) (unpublished manuscript)"},{"issue":"3","key":"3_CR20","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1145\/1071596.1071598","volume":"6","author":"M. Ferrari","year":"2005","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: On the complexity of the disjunction property in intuitionistic and modal logics. ACM Transactions on Computational Logic\u00a06(3), 519\u2013538 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"3_CR21","doi-asserted-by":"publisher","first-page":"113","DOI":"10.2307\/2271891","volume":"40","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: One hundred and two problems in mathematical logic. The Journal of Symbolic Logic\u00a040(2), 113\u2013129 (1975)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"3_CR22","doi-asserted-by":"publisher","first-page":"859","DOI":"10.2307\/2586506","volume":"64","author":"S. Ghilardi","year":"1999","unstructured":"Ghilardi, S.: Unification in intuitionistic logic. The Journal of Symbolic Logic\u00a064(2), 859\u2013880 (1999)","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"3_CR23","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1093\/logcom\/2.3.397","volume":"2","author":"G. Gottlob","year":"1992","unstructured":"Gottlob, G.: Complexity results for nonmonotonic logics. Journal of Logic and Computation\u00a02(3), 397\u2013425 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.apal.2007.01.001","volume":"146","author":"P. Hrube\u0161","year":"2007","unstructured":"Hrube\u0161, P.: A lower bound for intuitionistic logic. Annals of Pure and Applied Logic\u00a0146(1), 72\u201390 (2007)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"3_CR26","doi-asserted-by":"publisher","first-page":"941","DOI":"10.2178\/jsl\/1191333849","volume":"72","author":"P. Hrube\u0161","year":"2007","unstructured":"Hrube\u0161, P.: Lower bounds for modal logics. The Journal of Symbolic Logic\u00a072(3), 941\u2013958 (2007)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2-3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.apal.2008.09.013","volume":"157","author":"P. Hrube\u0161","year":"2009","unstructured":"Hrube\u0161, P.: On lengths of proofs in non-classical logics. Annals of Pure and Applied Logic\u00a0157(2-3), 194\u2013205 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"3_CR28","doi-asserted-by":"publisher","first-page":"281","DOI":"10.2307\/2694922","volume":"66","author":"R. Iemhoff","year":"2001","unstructured":"Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. The Journal of Symbolic Logic\u00a066(1), 281\u2013294 (2001)","journal-title":"The Journal of Symbolic Logic"},{"issue":"4","key":"3_CR29","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1093\/logcom\/exi029","volume":"15","author":"E. Je\u0159\u00e1bek","year":"2005","unstructured":"Je\u0159\u00e1bek, E.: Admissible rules of modal logics. Journal of Logic and Computation\u00a015(4), 411\u2013431 (2005)","journal-title":"Journal of Logic and Computation"},{"key":"3_CR30","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1016\/j.apal.2006.04.001","volume":"142","author":"E. Je\u0159\u00e1bek","year":"2006","unstructured":"Je\u0159\u00e1bek, E.: Frege systems for extensible modal logics. Annals of Pure and Applied Logic\u00a0142, 366\u2013379 (2006)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"3_CR31","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s00153-006-0028-9","volume":"46","author":"E. Je\u0159\u00e1bek","year":"2007","unstructured":"Je\u0159\u00e1bek, E.: Complexity of admissible rules. Archive for Mathematical Logic\u00a046(2), 73\u201392 (2007)","journal-title":"Archive for Mathematical Logic"},{"issue":"1-2","key":"3_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2008.10.005","volume":"159","author":"E. Je\u0159\u00e1bek","year":"2009","unstructured":"Je\u0159\u00e1bek, E.: Substitution Frege and extended Frege proof systems in non-classical logics. Annals of Pure and Applied Logic\u00a0159(1-2), 1\u201348 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Je\u0159\u00e1bek, E.: Admissible rules of \u0141ukasiewicz logic. Journal of Logic and Computation (to appear, 2010)","DOI":"10.1093\/logcom\/exp078"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Je\u0159\u00e1bek, E.: Bases of admissible rules of \u0141ukasiewicz logic. Journal of Logic and Computation (to appear, 2010)","DOI":"10.1093\/logcom\/exp078"},{"issue":"3","key":"3_CR35","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.2307\/2274765","volume":"54","author":"J. Kraj\u00ed\u010dek","year":"1989","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. The Journal of Symbolic Logic\u00a054(3), 1063\u20131079 (1989)","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"3_CR36","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1006\/inco.1997.2674","volume":"140","author":"J. Kraj\u00ed\u010dek","year":"1998","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: Some consequences of cryptographical conjectures for $S^1_2$ and EF. Information and Computation\u00a0140(1), 82\u201394 (1998)","journal-title":"Information and Computation"},{"issue":"1","key":"3_CR37","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1002\/rsa.3240070103","volume":"7","author":"J. Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P., Woods, A.: Exponential lower bounds to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures and Algorithms\u00a07(1), 15\u201339 (1995)","journal-title":"Random Structures and Algorithms"},{"key":"3_CR38","series-title":"Encyclopedia of Mathematics and Its Applications","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory","author":"J. Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications, vol.\u00a060. Cambridge University Press, Cambridge (1995)"},{"issue":"2","key":"3_CR39","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic\u00a062(2), 457\u2013486 (1997)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"3_CR40","doi-asserted-by":"publisher","first-page":"197","DOI":"10.2307\/2687774","volume":"7","author":"J. Kraj\u00ed\u010dek","year":"2001","unstructured":"Kraj\u00ed\u010dek, J.: Tautologies from pseudo-random generators. Bulletin of Symbolic Logic\u00a07(2), 197\u2013212 (2001)","journal-title":"Bulletin of Symbolic Logic"},{"issue":"1","key":"3_CR41","doi-asserted-by":"publisher","first-page":"265","DOI":"10.2178\/jsl\/1080938841","volume":"69","author":"J. Kraj\u00ed\u010dek","year":"2004","unstructured":"Kraj\u00ed\u010dek, J.: Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds. The Journal of Symbolic Logic\u00a069(1), 265\u2013286 (2004)","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"3_CR42","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R.E. Ladner","year":"1977","unstructured":"Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing\u00a06(3), 467\u2013480 (1977)","journal-title":"SIAM Journal on Computing"},{"issue":"5","key":"3_CR43","doi-asserted-by":"publisher","first-page":"2392","DOI":"10.1007\/s10958-006-0116-8","volume":"134","author":"G. Mints","year":"2006","unstructured":"Mints, G., Kojevnikov, A.: Intuitionistic Frege systems are polynomially equivlalent. Journal of Mathematical Sciences\u00a0134(5), 2392\u20132402 (2006)","journal-title":"Journal of Mathematical Sciences"},{"key":"3_CR44","unstructured":"Pitassi, T., Santhanam, R.: Effectively polynomial simulations. In: Proc. 1st Innovations in Computer Science (2010)"},{"issue":"3","key":"3_CR45","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. The Journal of Symbolic Logic\u00a062(3), 981\u2013998 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"3_CR46","first-page":"1033","volume":"282","author":"A.A. Razborov","year":"1985","unstructured":"Razborov, A.A.: Lower bounds on the monotone complexity of boolean functions. Doklady Akademii Nauk SSSR\u00a0282, 1033\u20131037 (1985); English translation in: Soviet Math. Doklady 31, 354\u2013357","journal-title":"Doklady Akademii Nauk SSSR"},{"issue":"4","key":"3_CR47","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s000370050013","volume":"7","author":"A.A. Razborov","year":"1998","unstructured":"Razborov, A.A.: Lower bounds for the polynomial calculus. Computational Complexity\u00a07(4), 291\u2013324 (1998)","journal-title":"Computational Complexity"},{"key":"3_CR48","unstructured":"Reckhow, R.A.: On the lengths of proofs in the propositional calculus. PhD thesis, University of Toronto (1976)"},{"key":"3_CR49","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R. Reiter","year":"1980","unstructured":"Reiter, R.: A logic for default reasoning. Artificial Intelligence\u00a013, 81\u2013132 (1980)","journal-title":"Artificial Intelligence"},{"key":"3_CR50","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(97)80001-8","volume-title":"Admissibility of logical inference rules","author":"V.V. Rybakov","year":"1997","unstructured":"Rybakov, V.V.: Admissibility of logical inference rules. Studies in Logic and the Foundations of Mathematics, vol.\u00a0136. Elsevier, Amsterdam (1997)"},{"issue":"4","key":"3_CR51","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. Bulletin of Symbolic Logic\u00a013(4), 417\u2013481 (2007)","journal-title":"Bulletin of Symbolic Logic"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Tseitin, G.C.: On the complexity of derivations in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Mathematics and Mathematical Logic, Part II, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"3_CR53","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03927-4","volume-title":"Introduction to Circuit Complexity \u2013 A Uniform Approach","author":"H. Vollmer","year":"1999","unstructured":"Vollmer, H.: Introduction to Circuit Complexity \u2013 A Uniform Approach. Texts in Theoretical Computer Science. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13562-0_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:40:05Z","timestamp":1606167605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13562-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642135613","9783642135620"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13562-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}