{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:52:40Z","timestamp":1760079160460},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[1995,12,1]],"date-time":"1995-12-01T00:00:00Z","timestamp":817776000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch Math Logic"],"published-print":{"date-parts":[[1995,12]]},"DOI":"10.1007\/bf02391554","type":"journal-article","created":{"date-parts":[[2006,5,12]],"date-time":"2006-05-12T17:48:55Z","timestamp":1147456135000},"page":"377-394","source":"Crossref","is-referenced-by-count":16,"title":["Some remarks on lengths of propositional proofs"],"prefix":"10.1007","volume":"34","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02391554_CR1","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1093\/oso\/9780198536901.003.0004","volume-title":"Arithmetic, Proof Theory and Computational Complexity","author":"M.L. Bonet","year":"1993","unstructured":"Bonet, M.L.: Number of symbols in Frege proofs with and without the deduction rule. In: Clote, P., Kraj\u00ed\u010dek, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 61\u201395. Oxford: Oxford University Press 1993"},{"key":"BF02391554_CR2","doi-asserted-by":"crossref","first-page":"688","DOI":"10.2307\/2275228","volume":"58","author":"M.L. Bonet","year":"1993","unstructured":"Bonet, M.L., Buss, S.R.: The deduction rule and linear and near-linear proof simulations. J. Symb. Logic58, 688\u2013709 (1993)","journal-title":"J. Symb. Logic"},{"key":"BF02391554_CR3","doi-asserted-by":"crossref","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"S.R. Buss","year":"1987","unstructured":"Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Logic52, 916\u2013927 (1987)","journal-title":"J. Symb. Logic"},{"key":"BF02391554_CR4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","volume":"53","author":"S.R. Buss","year":"1991","unstructured":"Buss, S.R.: The undecidability ofk-provability. Ann. Pure Appl. Logic53, 75\u2013102 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"BF02391554_CR5","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-1-4612-2566-9_4","volume-title":"Feasible Mathematics vol. II","author":"S.R. Buss","year":"1995","unstructured":"Buss, S.R.: On G\u00f6del\u2019s theorems on lengths of proofs II: Lower bounds for recognizingk symbol provability. In: Clote, P., Remmel, J. (eds.) Feasible Mathematics vol. II, pp. 57\u201390 Boston: Birkh\u00e4user 1995"},{"key":"BF02391554_CR6","unstructured":"Buss, S.R., et al.: Weak formal systems and connections to computational complexity. Student-written Lecture Notes for a Topics Course at U.C. Berkeley, January\u2013May (1988)"},{"key":"BF02391554_CR7","first-page":"57","volume":"8","author":"G. Cejtin","year":"1975","unstructured":"Cejtin, G., \u010cubarjan, A.: On some bounds to the lengths of logical proofs in classical propositional calculus (Russian). Trudy Vy\u010disl. Centra AN ArmSSR i Erevan. Univ.8, 57\u201364 (1975)","journal-title":"Trudy Vy\u010disl. Centra AN ArmSSR i Erevan. Univ."},{"key":"BF02391554_CR8","doi-asserted-by":"crossref","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. J. Symb. Logic44, 36\u201350 (1979)","journal-title":"J. Symb. Logic"},{"key":"BF02391554_CR9","unstructured":"Dowd, M.: Model-theoretic aspects ofP \u2260NP. Typewritten manuscript (1985)"},{"key":"BF02391554_CR10","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(89)90012-2","volume":"41","author":"J. Kraj\u00ed\u010dek","year":"1989","unstructured":"Kraj\u00ed\u010dek, J.: On the number of steps in proofs. Ann. Pure Appl. Logic41, 153\u2013178 (1989)","journal-title":"Ann. Pure Appl. Logic"},{"key":"BF02391554_CR11","first-page":"137","volume":"30","author":"J. Kraj\u00ed\u010dek","year":"1989","unstructured":"Kraj\u00ed\u010dek, J.: Speed-up for propositional Frege systems via generalizations of proofs. Commentationes Mathematicae Universitatis Carolinae30, 137\u2013140 (1989)","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"BF02391554_CR12","doi-asserted-by":"crossref","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, J. Symb. Logic54, 1063\u20131079 (1989)","journal-title":"J. Symb. Logic"},{"key":"BF02391554_CR13","doi-asserted-by":"crossref","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P., Woods, A.: Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Struct. Algorithms (to appear)","DOI":"10.1002\/rsa.3240070103"},{"key":"BF02391554_CR14","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01200117","volume":"3","author":"T. Pitassi","year":"1993","unstructured":"Pitassi, T., Beame, P., Impagliazzo, R.: Exponential lower bounds for the pigeonhole principle. Comput. Complex.3, 97\u2013140 (1993)","journal-title":"Comput. Complex."},{"key":"BF02391554_CR15","unstructured":"Reckhow, R.A.: On the lengths of proofs in the propositional calculus. PhD thesis, Department of Computer Science, University of Toronto, Technical Report #87 (1976)"},{"key":"BF02391554_CR16","first-page":"505","volume-title":"Logic Colloquium \u201976","author":"R. Statman","year":"1977","unstructured":"Statman, R.: Complexity of derivations from quantifier-free Horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems. In: Logic Colloquium \u201976, pp. 505\u2013517. Amsterdam: North Holland 1977"},{"key":"BF02391554_CR17","volume-title":"Proof Theory","author":"G. Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory, 2nd edn. Amsterdam: North-Holland 1987","edition":"2nd edn."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02391554.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02391554\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02391554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T11:23:28Z","timestamp":1707045808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02391554"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":17,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["BF02391554"],"URL":"https:\/\/doi.org\/10.1007\/bf02391554","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}