{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:16:46Z","timestamp":1725664606216},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614401"},{"type":"electronic","value":"9783540685807"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61440-0_116","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:38:26Z","timestamp":1330292306000},"page":"48-62","source":"Crossref","is-referenced-by-count":11,"title":["Lower bounds for prepositional proofs and independence results in bounded arithmetic"],"prefix":"10.1007","author":[{"given":"Alexander A.","family":"Razborov","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"M. Ajtai. The complexity of the pigeonhole principle. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 346\u2013355, 1988.","DOI":"10.1109\/SFCS.1988.21951"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"M. Ajtai. Parity and the pigeonhole principle. In S. R. Buss and P. J. Scott, editors, Feasible Mathematics, pages 1\u201324. Birkhauser, 1990.","DOI":"10.1007\/978-1-4612-3466-1_1"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"M. Ajtai. The independence of the modulo p counting principle. In Proceedings of the 26th ACM STOC, pages 402\u2013411, 1994.","DOI":"10.1145\/195058.195207"},{"issue":"1","key":"4_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02579196","volume":"7","author":"N. Alon","year":"1987","unstructured":"N. Alon and R. Boppana. The monotone circuit complexity of Boolean functions. Combinatorica, 7(1):1\u201322, 1987.","journal-title":"Combinatorica"},{"key":"4_CR5","unstructured":"P. Beame, R. Impagliazzo, J. Kraj\u00ed\u010dek, T. Pitassi, and P. Pudl\u00e1k. Lower bounds on Hilbert's Nullstellensatz and propositional proofs. To appear in Proc. of the London Math. Soc., 1994."},{"key":"4_CR6","unstructured":"P. Beame and T. Pitassi. Exponential separation between the matching principles and the pigeonhole principle. Submitted to Annals of Pure and Applied Logic, 1993."},{"issue":"6","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1161","DOI":"10.1137\/0221068","volume":"21","author":"S. Bellantoni","year":"1992","unstructured":"S. Bellantoni, T. Pitassi, and A. Urquhart. Approximation of small depth Frege proofs. SIAM Journal on Computing, 21(6):1161\u20131179, 1992.","journal-title":"SIAM Journal on Computing"},{"key":"4_CR8","unstructured":"A. Blake. Canonical expressions in Boolean algebra. PhD thesis, University of Chicago, 1937."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"M. Bonet, T. Pitassi, and R. Raz. Lower bounds for cutting planes proofs with small coefficients. In Proceedings of the 27th ACM STOC, pages 575\u2013584, 1995.","DOI":"10.1145\/225058.225275"},{"key":"4_CR10","volume-title":"Bounded Arithmetic","author":"S. R. Buss","year":"1986","unstructured":"S. R. Buss. Bounded Arithmetic. Bibliopolis, Napoli, 1986."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"S. Buss, R. Impagliazzo, J. Kraj\u00ed\u010dek, P. Pudl\u00e1k, A. Razborov, and J. Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Submitted to Computational Complexity, 1996.","DOI":"10.1007\/BF01294258"},{"issue":"4","key":"4_CR12","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"V. Chv\u00e1tal and E. Szemer\u00e9di. Many hard examples for resolution. Journal of the ACM, 35(4):759\u2013768, 1988.","journal-title":"Journal of the ACM"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"S. A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the 7th Annual ACM Symposium on the Theory of Computing, pages 83\u201397, 1975.","DOI":"10.1145\/800116.803756"},{"issue":"1","key":"4_CR14","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. A. Cook","year":"1979","unstructured":"S. A. Cook and A. R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36\u201350, 1979.","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"W. Cook, C. R. Coullard, and G. Tur\u00e1n. On the complexity of cutting plane proofs. Discrete Applied Mathematics, 18:25\u201338, 1987.","journal-title":"Discrete Applied Mathematics"},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):210\u2013215, 1960.","journal-title":"Journal of the ACM"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"P. H\u00e1jek and P. Pudl\u00e1k. Metamathematics of First-Order Arithmetic. Springer-Verlag, 1993.","DOI":"10.1007\/978-3-662-22156-3"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"A. Haken. The intractability or fesolution. Theoretical Computer Science, 39:297\u2013308, 1985.","journal-title":"Theoretical Computer Science"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"A. Haken. Counting bottlenecks to show monotone P \u2260 NP. In Proceedings of the 36th IEEE FOCS, 1995.","DOI":"10.1109\/SFCS.1995.492460"},{"key":"4_CR20","unstructured":"J. H\u00e5stad. Computational limitations on Small Depth Circuits. PhD thesis, Massachusetts Institute of Technology, 1986."},{"issue":"1","key":"4_CR21","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2275250","volume":"59","author":"J. Kraj\u00ed\u010dek","year":"1994","unstructured":"J. Kraj\u00ed\u010dek. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 59(1):73\u201386, 1994.","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. Bounded arithmetic, propositional logic and complexity theory. Cambridge University Press, 1994.","DOI":"10.1017\/CBO9780511529948"},{"key":"4_CR23","unstructured":"J. Kraj\u00ed\u010dek. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. To appear in Journal of Symbolic Logic, 1994."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek and P. Pudl\u00e1k. Some consequences of cryptographical conjectures for S 2 1 and EF. To appear in the Proceedings of the meeting Logic and Computational Complexity, Ed. D. Leivant, 1995.","DOI":"10.1007\/3-540-60178-3_86"},{"issue":"1","key":"4_CR25","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1002\/rsa.3240070103","volume":"7","author":"J. Kraj\u00ed\u010dek","year":"1995","unstructured":"J. Kraj\u00ed\u010dek, P. Pudl\u00e1k, and A. R. Woods. Exponential lower bounds to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms, 7(1):15\u201339, 1995.","journal-title":"Random Structures and Algorithms"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01200117","volume":"3","author":"T. Pitassi","year":"1993","unstructured":"T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3:97\u2013140, 1993.","journal-title":"Computational Complexity"},{"key":"4_CR27","unstructured":"P. Pudl\u00e1k. Lower bounds for resolution and cutting planes proofs and monotone computations. Submitted to Journal of Symbolic Logic, 1995."},{"issue":"4","key":"4_CR28","first-page":"598","volume":"41","author":"\u0410. \u0410. \u0420\u0430\u0437\u0431\u043e\u0440\u043e\u0432","year":"1987","unstructured":"\u0410. \u0410. \u0420\u0430\u0437\u0431\u043e\u0440\u043e\u0432. \u041d\u0438\u0436\u043d \u0438\u0435 \u043e\u0446\u0435\u043d\u043a\u0438 \u0440\u0430\u0437\u043c\u0435\u0440\u0430 \u0441\u0445\u0435 \u043c \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e\u0439 \u0433\u043b\u0443\u0431\u0438 \u043d\u044b \u0432 \u043f\u043e\u043b\u043d\u043e\u043c \u0431\u0430\u0437\u0438\u0441\u0435, \u0441\u043e\u0434 \u0435\u0440\u0436\u0430\u0449\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u043b\u043e\u0433\u0438 \u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0441\u043b\u043e\u0436\u0435\u043d\u0438\u044f. \u041c\u0430 \u0442\u0435\u043c. \u0417\u0430\u043c., 41(4):598\u2013607, 1987. A. A. Razborov, Lower bounds on the size of bounded-depth networks over a complete basis with logical addition, Mathem. Notes of the Academy of Sci. of the USSR, 41(4):333\u2013338, 1987.","journal-title":"\u041c\u0430 \u0442\u0435\u043c. \u0417\u0430\u043c."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"A. Razborov. An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic. In P. Clote and J. Kraj\u00ed\u010dek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 247\u2013277. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198536901.003.0012"},{"key":"4_CR30","first-page":"42","volume-title":"Lecture Notes in Computer Science, 621","author":"A. Razborov","year":"1992","unstructured":"A. Razborov. On small depth threshold circuits. In Proceedings of the SWAT 92, Lecture Notes in Computer Science, 621, pages 42\u201352, New York\/Berlin, 1992. Springer-Verlag."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"A. Razborov. Bounded Arithmetic and lower bounds in Boolean complexity. In P. Clote and J. Remmel, editors, Feasible Mathematics II. Progress in Computer Science and Applied Logic, vol. 13, pages 344\u2013386. Birkha\u00fcser, 1995.","DOI":"10.1007\/978-1-4612-2566-9_12"},{"issue":"1","key":"4_CR32","first-page":"201","volume":"59","author":"A. Razborov","year":"1995","unstructured":"A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of Bounded Arithmetic. \u0418\u0437 \u0432. \u0410\u041d \u0421\u0421\u0421\u0420, \u0441\u0435\u0440. \u043c\u0430\u0442\u0435\u043c. (Izvestiya of the RAN), 59(1):201\u2013222, 1995. See also Izvestiya: Mathematics 59:1, 205\u2013227.","journal-title":"\u0418\u0437 \u0432. \u0410\u041d \u0421\u0421\u0421\u0420, \u0441\u0435\u0440. \u043c\u0430\u0442\u0435\u043c. (Izvestiya of the RAN)"},{"key":"4_CR33","volume-title":"Technical Report RS-94-36","author":"A. Razborov","year":"1994","unstructured":"A. Razborov. On provably disjoint NP-pairs. Technical Report RS-94-36, Basic Research in Computer Science Center, Aarhus, Denmark, 1994."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"A. Razborov and S. Rudich. Natural proofs. To appear in Journal of Computer and System Sciences (for the preliminary version see Proceedings of the 26th ACM Symposium on Theory of Computing, pp. 204\u2013213), 1994.","DOI":"10.1145\/195058.195134"},{"key":"4_CR35","unstructured":"R. A. Reckhow. On the lengths of proofs in the propositional calculus. Technical Report 87, University of Toronto, 1976."},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"S. Riis. Independence in Bounded Arithmetic. PhD thesis, Oxford University, 1993.","DOI":"10.7146\/brics.v1i23.21644"},{"key":"4_CR37","volume-title":"Technical Report RS-94-21","author":"S. Riis","year":"1994","unstructured":"S. Riis. Count(q) does not imply Count(p). Technical Report RS-94-21, Basic Research in Computer Science Center, Aarhus, Denmark, 1994."},{"issue":"1","key":"4_CR38","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"4_CR39","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1090\/psapm\/038\/1020811","volume":"38","author":"A. L. Selman","year":"1989","unstructured":"A. L. Selman. Complexity issues in cryptography. Proceedings of Symposia in Applied Mathematics, 38:92\u2013107, 1989.","journal-title":"Proceedings of Symposia in Applied Mathematics"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"R. Smolensky. Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In Proceedings of the 19th ACM Symposium on Theory of Computing, pages 77\u201382, 1987.","DOI":"10.1145\/28395.28404"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"G. Takeuti. RSUV isomorphisms. In P. Clote and J. Kraj\u00ed\u010dek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 364\u2013386. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198536901.003.0016"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"\u0413. \u0421. \u0426\u0435\u0439\u0442\u0438\u043d. \u041e \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442 \u0438 \u0432\u044b\u0432\u043e\u0434\u0430 \u0432 \u0438\u0441\u0447\u0438\u0441\u043b\u0435\u043d\u0438\u0438 \u0432\u044b\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u043d\u0438\u0439, In \u0410. \u041e. \u0421\u043b\u0438 \u0441\u0435\u043d\u043a\u043e, editor, \u0418\u0441\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u043d\u0438\u044f \u043f\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u0438\u0432\u043d\u043e\u0439 \u043c\u0430 \u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0435 \u0438 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447 \u0435\u0441\u043a\u043e\u0439 \u043b\u043e\u0433\u0438\u043a\u0435, II; \u0417\u0430\u043f\u0438\u0441\u043a \u0438\u043d\u0430\u0443\u0447\u043d\u044b\u0445 \u0441\u0435\u043c\u0438\u043d\u0430\u0440\u043e\u0432 \u041b \u041e\u041c\u0418, m. 8, pages 234\u2013259. \u041d\u0430\u0443\u043a\u0430, \u041b\u0435\u043d\u0438\u043d\u0433 \u0440\u0430\u0434, 1968. Engl. translation: G. C. Tseitin, On the complexity of derivations in propositional calculus, in: Studies in mathematics and mathematical logic, Part II, ed. A. O. Slissenko, pp. 115\u2013125.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"issue":"1","key":"4_CR43","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"A. Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209\u2013219, 1987.","journal-title":"Journal of the ACM"},{"key":"4_CR44","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"A. Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1:425\u2013467, 1995.","journal-title":"Bulletin of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61440-0_116.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:28:34Z","timestamp":1713634114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61440-0_116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614401","9783540685807"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/3-540-61440-0_116","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}