{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:10:36Z","timestamp":1737436236730,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_38","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T12:03:26Z","timestamp":1187265806000},"page":"569-583","source":"Crossref","is-referenced-by-count":9,"title":["On the Automatizability of Resolution and Related Propositional Proof Systems"],"prefix":"10.1007","author":[{"given":"Albert","family":"Atserias","sequence":"first","affiliation":[]},{"given":"Mar\u00eda Luisa","family":"Bonet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"M. Alekhnovich and A. A. Razborov. Resolution is not automatizable unless W[P] is tractable. In 42nd Annual IEEE Symposium on Foundations of Computer Science, 2001.","DOI":"10.1109\/SFCS.2001.959895"},{"key":"38_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02579196","volume":"7","author":"N. Alon","year":"1987","unstructured":"N. Alon and R. B. Boppana. The monotone circuit complexity of boolean functions. Combinatorica, 7:1\u201322, 1987.","journal-title":"Combinatorica"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"A. Atserias and M. L. Bonet. On the automatizability of resolution and related propositional proof systems. ECCC TR02-010, 2002.","DOI":"10.1007\/3-540-45793-3_38"},{"key":"38_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1007\/3-540-48224-5_81","volume-title":"Information and Computation","author":"A. Atserias","year":"2001","unstructured":"A. Atserias, M. L. Bonet, and J.L. Esteban. Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Accepted for publication in Information and Computation. A preliminary version appeared in ICALP\u201901, Lecture Notes in Computer Science 2076, Springer, pages 1005\u20131016., 2001."},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In 37th Annual IEEE Symposium on Foundations of Computer Science, pages 274\u2013282, 1996.","DOI":"10.1109\/SFCS.1996.548486"},{"key":"38_CR6","unstructured":"E. Ben-Sasson, R. Impagliazzo, and A. Wigderson. Near-optimal separation of general and tree-like resolution. To appear, 2002."},{"issue":"2","key":"38_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E. Ben-Sasson","year":"2001","unstructured":"E. Ben-Sasson and A. Wigderson. Short proofs are narrow-resolution made simple. J. ACM, 48(2):149\u2013169, 2001.","journal-title":"J. ACM"},{"key":"38_CR8","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/0020-0190(81)90050-8","volume":"13","author":"M. Blum","year":"1981","unstructured":"M. Blum, R. M. Karp, O. Vornberger, C. H. Papadimitriou, and M. Yannakakis. The complexity of testing whether a graph is a superconcentrator. Information Processing Letter, 13:164\u2013167, 1981.","journal-title":"Information Processing Letter"},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"M. L. Bonet, C. Domingo, R. Gavald\u00e0, A. Maciel, and T. Pitassi. Non-automatizability of bounded-depth Frege proofs. In 14th IEEE Conference on Computational Complexity, pages 15\u201323, 1999. Accepted for publication in the Journal of Computational Complexity.","DOI":"10.1109\/CCC.1999.766258"},{"issue":"5","key":"38_CR10","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1137\/S0097539799352474","volume":"30","author":"M. L. Bonet","year":"2000","unstructured":"M. L. Bonet, J. L. Esteban, N. Galesi, and J. Johansen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Journal of Computing, 30(5):1462\u20131484, 2000. A preliminary version appeared in FOCS\u201998.","journal-title":"SIAM Journal of Computing"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"M. L. Bonet and N. Galesi. Optimality of size-width trade-offs for resolution. Journal of Computational Complexity, 2001. To appear. A preliminary version appeared in FOCS\u201999.","DOI":"10.1007\/s000370100000"},{"issue":"3","key":"38_CR12","doi-asserted-by":"publisher","first-page":"708","DOI":"10.2307\/2275569","volume":"62","author":"M. L. Bonet","year":"1997","unstructured":"M. L. Bonet, T. Pitassi, and R. Raz. Lower bounds for cutting planes proofs with small coefficients. Journal of Symbolic Logic, 62(3):708\u2013728, 1997. A preliminary version appeared in STOC\u201995.","journal-title":"Journal of Symbolic Logic"},{"issue":"6","key":"38_CR13","doi-asserted-by":"publisher","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M. L. Bonet","year":"2000","unstructured":"M. L. Bonet, T. Pitassi, and R. Raz. On interpolation and automatization for Frege systems. SIAM Journal of Computing, 29(6):1939\u20131967, 2000. A preliminary version appeared in FOCS\u201997.","journal-title":"SIAM Journal of Computing"},{"key":"38_CR14","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. Cook","year":"1979","unstructured":"S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44:36\u201350, 1979.","journal-title":"Journal of Symbolic Logic"},{"key":"38_CR15","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1006\/jcss.1998.1617","volume":"58","author":"S.A. Cook","year":"1999","unstructured":"S.A. Cook and A. Haken. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences, 58:326\u2013335, 1999.","journal-title":"Journal of Computer and System Sciences"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"S. Dantchev and S. Riis. Tree resolution proofs of the weak pigeon-hole principle. In 16th IEEE Conference on Computational Complexity, pages 69\u201375, 2001.","DOI":"10.1109\/CCC.2001.933873"},{"key":"38_CR17","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"38_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7:201\u2013215, 1960.","journal-title":"J. ACM"},{"key":"38_CR19","unstructured":"J. L. Esteban, N. Galesi, and J. Messner. Personal communication. Manuscript, 2001."},{"key":"38_CR20","doi-asserted-by":"crossref","unstructured":"R. Impagliazzo, T. Pitassi, and A. Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In 9th IEEE Symposium on Logic in Computer Science, pages 220\u2013228, 1994.","DOI":"10.1109\/LICS.1994.316069"},{"issue":"1","key":"38_CR21","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2275250","volume":"39","author":"J. Kraj\u00edcek","year":"1994","unstructured":"J. Kraj\u00edcek. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 39(1):73\u201386, 1994.","journal-title":"Journal of Symbolic Logic"},{"key":"38_CR22","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00edcek","year":"1997","unstructured":"J. Kraj\u00edcek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, 62:457\u2013486, 1997.","journal-title":"Journal of Symbolic Logic"},{"key":"38_CR23","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00edcek. On the weak pigeonhole principle. To appear in Fundamenta Mathematic\u00e6, 2000.","DOI":"10.4064\/fm170-1-8"},{"issue":"1","key":"38_CR24","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1006\/inco.1997.2674","volume":"140","author":"J. Kraj\u00edcek","year":"1998","unstructured":"J. Kraj\u00edcek and P. Pudl\u00e1k. Some consequences of cryptographical conjectures for S 2 1 and EF. Information and Computation, 140(1):82\u201394, 1998.","journal-title":"Information and Computation"},{"key":"38_CR25","doi-asserted-by":"crossref","unstructured":"A. Maciel, T. Pitassi, and A.R. Woods. A new proof of the weak pigeonhole principle. In 32nd Annual ACM Symposium on the Theory of Computing, 2000.","DOI":"10.1145\/335305.335348"},{"issue":"3","key":"38_CR26","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"P. Pudl\u00e1k. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3):981\u2013998, 1997.","journal-title":"Journal of Symbolic Logic"},{"key":"38_CR27","doi-asserted-by":"crossref","unstructured":"P. Pudl\u00e1k. On the complexity of the propositional calculus. In Sets and Proofs, Invited Papers from Logic Colloquium\u2019 97, pages 197\u2013218. Cambridge University Press, 1999.","DOI":"10.1017\/CBO9781107325944.010"},{"key":"38_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1007\/3-540-44683-4_54","volume-title":"26th International Symposium on Mathematical Foundations of Computer Science","author":"P. Pudl\u00e1k","year":"2001","unstructured":"P. Pudl\u00e1k. On reducibility and symmetry of disjoint NP-pairs. In 26th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, pages 621\u2013632. Springer-Verlag, 2001."},{"key":"38_CR29","doi-asserted-by":"crossref","unstructured":"P. Pudl\u00e1k and J. Sgall. Algebraic models of computation and interpolation for algebraic proof systems. In P. W. Beame and S.R. Buss, editors, Proof Complexity and Feasible Arithmetic, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279\u2013296. American Mathematical Society, 1998.","DOI":"10.1090\/dimacs\/039\/15"},{"issue":"1","key":"38_CR30","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1070\/IM1995v059n01ABEH000009","volume":"59","author":"A. A. Razborov","year":"1995","unstructured":"A. A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya of the RAN, 59(1):205\u2013227, 1995.","journal-title":"Izvestiya of the RAN"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T11:39:21Z","timestamp":1737373161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_38","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}