乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T21:11:16Z","timestamp":1717276276926},"reference-count":161,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":2237,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[2007,12]]},"abstract":"Abstract<\/jats:title>Propositional proof complexity is the study of the sizes of propositional proofs, and more generally, the resources necessary to certify propositional tautologies. Questions about proof sizes have connections with computational complexity, theories of arithmetic, and satisfiability algorithms. This is article includes a broad survey of the field, and a technical exposition of some recently developed techniques for proving lower bounds on proof sizes.<\/jats:p>","DOI":"10.2178\/bsl\/1203350879","type":"journal-article","created":{"date-parts":[[2008,3,25]],"date-time":"2008-03-25T18:39:20Z","timestamp":1206470360000},"page":"417-481","source":"Crossref","is-referenced-by-count":152,"title":["The Complexity of Propositional Proofs"],"prefix":"10.1017","volume":"13","author":[{"given":"Nathan","family":"Segerlind","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600001931_ref120","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45643-0_3"},{"key":"S1079898600001931_ref089","unstructured":"Hertel P. and Pitassi T. , An exponential time\/space speedup for resolution, Technical Report TR07-046, Electronic Colloquium on Computational Complexity, 2007."},{"key":"S1079898600001931_ref145","unstructured":"Razborov A. , Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution, Submitted to the Journal of Glacial Refereeing. Manuscript available at http:\/\/genesis.mi.ras.ru\/~razborov\/, 2003."},{"key":"S1079898600001931_ref105","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"S1079898600001931_ref100","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S1079898600001931_ref092","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316069"},{"key":"S1079898600001931_ref130","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"S1079898600001931_ref107","first-page":"193","volume-title":"Proceedings of the nineteenth annual IEEE symposium on foundations of computer science","author":"Lipton","year":"1978"},{"key":"S1079898600001931_ref098","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00058-0"},{"key":"S1079898600001931_ref062","first-page":"449","volume-title":"Proceedings of the seventeenth international conference on automated deduction","author":"Chatalic","year":"2000"},{"key":"S1079898600001931_ref039","unstructured":"Bennett J. H. , On spectra, Ph.D. thesis, Princeton University, 1962."},{"key":"S1079898600001931_ref155","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/28395.28404","volume-title":"Proceedings of the nineteenth annual ACM symposium on theory of computing","author":"Smolensky","year":"1987"},{"key":"S1079898600001931_ref067","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1090\/dimacs\/039\/06","volume-title":"Proof complexity and feasible mathematics","volume":"39","author":"Clote","year":"1998"},{"key":"S1079898600001931_ref136","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90110-4"},{"key":"S1079898600001931_ref036","first-page":"415","volume-title":"Fortieth annual IEEE symposium on foundations of computer science","author":"Ben-Sasson","year":"1999"},{"key":"S1079898600001931_ref014","first-page":"131","volume-title":"Eleventh IEEE\/ACM workshop on logic and synthesis","author":"Aloul","year":"2002"},{"key":"S1079898600001931_ref073","first-page":"635","volume-title":"Proceedings of the eighteenth national conference on artificial intelligence","author":"Dixon","year":"2002"},{"key":"S1079898600001931_ref142","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00453-X"},{"key":"S1079898600001931_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9006-x"},{"key":"S1079898600001931_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF01302964"},{"key":"S1079898600001931_ref056","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1726"},{"key":"S1079898600001931_ref022","first-page":"77","volume-title":"Tenth international conference on principles and practice of constraint programming","author":"Atserias","year":"2004"},{"key":"S1079898600001931_ref021","first-page":"239","volume-title":"Proceedings of the eighteenth annual IEEE conference on computational complexity","author":"Atserias","year":"2003"},{"key":"S1079898600001931_ref033","first-page":"13","volume-title":"Proof complexity and feasible arithmetics","author":"Beame","year":"1998"},{"key":"S1079898600001931_ref045","volume-title":"Handbook of theoretical computer science, volume A","author":"Boppana","year":"1990"},{"key":"S1079898600001931_ref063","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2006.03.009"},{"key":"S1079898600001931_ref046","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"S1079898600001931_ref079","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2921"},{"key":"S1079898600001931_ref023","first-page":"1","volume-title":"Proof complexity and feasible arithmetics","author":"Avigad","year":"1997"},{"key":"S1079898600001931_ref099","doi-asserted-by":"publisher","DOI":"10.2307\/2275250"},{"key":"S1079898600001931_ref042","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"S1079898600001931_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"S1079898600001931_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2003.07.011"},{"key":"S1079898600001931_ref058","first-page":"149","volume-title":"Proceedings of the eleventh internation workshop on computer science logic","author":"Buss","year":"1997"},{"key":"S1079898600001931_ref032","doi-asserted-by":"crossref","first-page":"1176","DOI":"10.1007\/11523468_95","volume-title":"Proceedings of the thirty-second international colloquium on automata, languages, and programming","author":"Beame","year":"2005"},{"key":"S1079898600001931_ref028","first-page":"225","volume-title":"Proceedings of the eighteenth IEEE conference on computational complexity","author":"Beame","year":"2003"},{"key":"S1079898600001931_ref016","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.75"},{"key":"S1079898600001931_ref010","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700366735"},{"key":"S1079898600001931_ref135","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1090\/dimacs\/039\/15","volume-title":"Proof complexity and feasible arithmetics","volume":"39","author":"Pudl\u00e1k","year":"1998"},{"key":"S1079898600001931_ref076","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1613\/jair.1353","article-title":"Generalizing boolean satisfiability I: Background and survey of existing work","volume":"21","author":"Dixon","year":"2004","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1079898600001931_ref012","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1109\/SFCS.2001.959895","volume-title":"Proceedings of the forty-second annual symposium on foundations of computer science","author":"Alekhnovich","year":"2001"},{"key":"S1079898600001931_ref104","doi-asserted-by":"publisher","DOI":"10.2307\/2274765"},{"key":"S1079898600001931_ref086","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121264"},{"key":"S1079898600001931_ref071","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"S1079898600001931_ref047","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"S1079898600001931_ref052","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90036-L"},{"key":"S1079898600001931_ref020","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3114"},{"key":"S1079898600001931_ref004","unstructured":"Aharonov D. and Naveh T. , Quantum NP- a survey, Technical Report arXiv:quantph\/02-210077, arXiv.org, 2002."},{"key":"S1079898600001931_ref069","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"S1079898600001931_ref156","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.10.018"},{"key":"S1079898600001931_ref121","first-page":"373","volume-title":"Eleventh IEEE\/ACM workshop on logic and synthesis","author":"Motter","year":"2002"},{"key":"S1079898600001931_ref013","first-page":"18","article-title":"Lower bounds for polynomial calculus: non-binomial case","volume":"242","author":"Alekhnovich","year":"2003","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"S1079898600001931_ref138","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/73007.73023","volume-title":"Proceedings of the twenty first annual ACM symposium on theory of computing","author":"Razborov","year":"1989"},{"key":"S1079898600001931_ref112","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","volume":"5","author":"Martin","year":"1962","journal-title":"Communications of the ACM"},{"key":"S1079898600001931_ref027","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"S1079898600001931_ref026","doi-asserted-by":"publisher","DOI":"10.1090\/pcms\/010\/07"},{"key":"S1079898600001931_ref001","first-page":"139","volume-title":"Proceedings of the fifteenth annual ACM-SIAM symposium on discrete algorithms","author":"Achlioptas","year":"2004"},{"key":"S1079898600001931_ref017","first-page":"346","volume-title":"Proceedings of the fifth international conference on theory and applications of satisfiability testing","author":"Aloul","year":"2002"},{"key":"S1079898600001931_ref043","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-004-0183-5"},{"key":"S1079898600001931_ref015","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.816218"},{"key":"S1079898600001931_ref054","first-page":"59","volume-title":"Proof complexity and feasible arithmetics","author":"Buss","year":"1998"},{"key":"S1079898600001931_ref131","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0030-y"},{"key":"S1079898600001931_ref082","unstructured":"Galesi N. and Lauria M. , Extending polynomial calculus to k-DNF resolution, Technical Report 41, Electronic Colloquium on Computational Complexity, 2007."},{"key":"S1079898600001931_ref029","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"S1079898600001931_ref068","first-page":"107","volume-title":"Proceedings of the seventh annual ACM symposium on the theory of computing","author":"Cook","year":"1975"},{"key":"S1079898600001931_ref119","first-page":"530","volume-title":"Proceedings of the thirty-eighth design automation conference","author":"Moskewicz","year":"2001"},{"key":"S1079898600001931_ref018","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00394-8"},{"key":"S1079898600001931_ref051","doi-asserted-by":"publisher","DOI":"10.2307\/2273826"},{"key":"S1079898600001931_ref085","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1958-10224-4"},{"key":"S1079898600001931_ref031","first-page":"42","volume-title":"Current trends in theoretical computer science: Entering the 21st century","author":"Beame","year":"2001"},{"key":"S1079898600001931_ref003","first-page":"121","volume-title":"Principles and practice of constraint programming","author":"Aguirre","year":"2001"},{"key":"S1079898600001931_ref109","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021264516079"},{"key":"S1079898600001931_ref025","unstructured":"Beame P. , A switching lemma primer, Technical report, Department of Computer Science and Engineering, University of Washington, 1994."},{"key":"S1079898600001931_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.10.004"},{"key":"S1079898600001931_ref048","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-002-0171-6"},{"key":"S1079898600001931_ref057","doi-asserted-by":"publisher","DOI":"10.1007\/BF01294258"},{"key":"S1079898600001931_ref065","volume-title":"Model checking","author":"Clarke","year":"1999"},{"key":"S1079898600001931_ref083","volume-title":"Proceedings of date 2002","author":"Goldberg","year":"2002"},{"key":"S1079898600001931_ref007","first-page":"402","volume-title":"Proceedings of the twenty-sixth annual ACM symposium on the theory of computing","author":"Ajtai","year":"1994"},{"key":"S1079898600001931_ref055","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00030-X"},{"key":"S1079898600001931_ref075","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1613\/jair.1555","article-title":"Generalizing boolean satisfiability II: Theory","volume":"22","author":"Dixon","year":"2004","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1079898600001931_ref053","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59048-1_3"},{"key":"S1079898600001931_ref081","doi-asserted-by":"publisher","DOI":"10.1090\/S0894-0347-99-00305-7"},{"key":"S1079898600001931_ref125","volume-title":"The seventh international conference on theory and applications of satisfiability testing","author":"Pan","year":"2004"},{"key":"S1079898600001931_ref151","unstructured":"Segerlind N. , Nearly-exponential size lower bounds for symbolic quantifier elimination algorithms and OBDD-based proofs of unsatisfiability, Technical Report 9, Electronic Colloquium on Computational Complexity, 2007."},{"key":"S1079898600001931_ref041","doi-asserted-by":"publisher","DOI":"10.2307\/2275569"},{"key":"S1079898600001931_ref103","unstructured":"Kraj\u00ed\u010dek J. , An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams, Technical Report 7, Electronic Colloquium on Computational Complexity, 2007."},{"key":"S1079898600001931_ref064","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"S1079898600001931_ref009","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1145\/1060590.1060634","volume-title":"Proceedings of the thirty-seventh annual ACM symposium on theory of computing","author":"Alekhnovich","year":"2005"},{"key":"S1079898600001931_ref070","doi-asserted-by":"publisher","DOI":"10.1287\/moor.1050.0151"},{"key":"S1079898600001931_ref101","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"S1079898600001931_ref128","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200028061"},{"key":"S1079898600001931_ref072","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900001041"},{"key":"S1079898600001931_ref096","first-page":"10","article-title":"Lower bounds on static Lov\u00e1sz\u2013Schrijver calculus proofs for Tseitin tautologies","volume":"340","author":"Itsykson","year":"2006","journal-title":"Zapiski Nauchnyh Seminarov POMI"},{"key":"S1079898600001931_ref077","volume-title":"Proceedings of SAT 2003","author":"E\u00e9n","year":"2003"},{"key":"S1079898600001931_ref066","first-page":"174","volume-title":"Proceedings of the twenty-eighth annual ACM symposium on the theory of computing","author":"Clegg","year":"1996"},{"key":"S1079898600001931_ref059","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1585"},{"key":"S1079898600001931_ref044","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"S1079898600001931_ref050","volume-title":"Bounded arithmetic","volume":"3","author":"Buss","year":"1986"},{"key":"S1079898600001931_ref108","doi-asserted-by":"publisher","DOI":"10.1137\/0801013"},{"key":"S1079898600001931_ref030","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","article-title":"Towards understanding and harnessing the potential of clause learning","volume":"22","author":"Beame","year":"2004","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1079898600001931_ref034","doi-asserted-by":"publisher","DOI":"10.1109\/SCT.1991.160281"},{"key":"S1079898600001931_ref049","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2006.v002a004"},{"key":"S1079898600001931_ref038","doi-asserted-by":"publisher","DOI":"10.1145\/375827.375835"},{"key":"S1079898600001931_ref061","first-page":"2","volume-title":"Proceedings of the twelfth international conference on tools with artificial intelligence","author":"Chatalic","year":"2000"},{"key":"S1079898600001931_ref040","first-page":"422","volume-title":"Proceedings of the fortieth annual IEEE symposium on foundations of computer science","author":"Bonet","year":"1999"},{"key":"S1079898600001931_ref114","doi-asserted-by":"crossref","unstructured":"McMillan K. , Symbolic model checking, Ph.D. thesis, Carnegie Mellon, 1992.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"S1079898600001931_ref116","first-page":"1","volume-title":"Proceedings of eleventh international conference on tools and algorithms for construction and analysis of systems","author":"McMillan","year":"2005"},{"key":"S1079898600001931_ref143","unstructured":"Razborov A. , Improved resolution lower bounds for theweak pigeonhole principle, Technical Report 55, Electronic Colloquium on Computational Complexity, 2001."},{"key":"S1079898600001931_ref094","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1109\/SFCS.2001.959894","volume-title":"Proceedings of the forty-second annual IEEE symposium on foundations of computer science","author":"Impagliazzo","year":"2001"},{"key":"S1079898600001931_ref087","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S1079898600001931_ref139","doi-asserted-by":"crossref","unstructured":"Razborov A. , On provably disjoint NP pairs, Technical Report 6, Electronic Colloquium on Computational Complexity, 1994.","DOI":"10.7146\/brics.v1i36.21607"},{"key":"S1079898600001931_ref133","first-page":"197","volume-title":"Sets and proofs: Invited papers from logic colloquium '97","volume":"258","author":"Pudl\u00e1k","year":"1997"},{"key":"S1079898600001931_ref152","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703428555"},{"key":"S1079898600001931_ref102","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"S1079898600001931_ref124","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/1132516.1132590","volume-title":"Proceedings of the thirty-eighth annual ACM symposium on theory of computing","author":"Nordstr\u00f6m","year":"2006"},{"key":"S1079898600001931_ref060","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90072-2"},{"key":"S1079898600001931_ref115","first-page":"1","volume-title":"Proceedings of fifteenth internation conference on computer aided verification","author":"McMillan","year":"2003"},{"key":"S1079898600001931_ref088","first-page":"143","volume-title":"Advances in computing research","volume":"5","author":"H\u00e5stad","year":"1989"},{"key":"S1079898600001931_ref008","first-page":"251","volume-title":"Proceedings of the thirty-seventh annual ACM symposium on the theory of computing","author":"Alekhnovich","year":"2005"},{"key":"S1079898600001931_ref127","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075316"},{"key":"S1079898600001931_ref140","first-page":"201","article-title":"Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic","volume":"59","author":"Razborov","year":"1995","journal-title":"Izvestiya of the Russian Academy of Science and Mathematics"},{"key":"S1079898600001931_ref074","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1613\/jair.1656","article-title":"Generalizing boolean satisfiability III: Implementation","volume":"23","author":"Dixon","year":"2005","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S1079898600001931_ref141","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050013"},{"key":"S1079898600001931_ref095","doi-asserted-by":"publisher","DOI":"10.1145\/1131313.1131314"},{"key":"S1079898600001931_ref097","first-page":"88","volume-title":"Bulletin of the European Association for Theoretical Computer Science","author":"Kabanets","year":"2002"},{"key":"S1079898600001931_ref126","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"S1079898600001931_ref123","doi-asserted-by":"publisher","DOI":"10.1007\/BF02023010"},{"key":"S1079898600001931_ref137","doi-asserted-by":"publisher","DOI":"10.1145\/972639.972640"},{"key":"S1079898600001931_ref144","first-page":"100","volume-title":"Proceedings of the the fifth international conference on developments in language theory","author":"Razborov","year":"2001"},{"key":"S1079898600001931_ref153","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59971-2"},{"key":"S1079898600001931_ref093","doi-asserted-by":"publisher","DOI":"10.1007\/s000370050024"},{"key":"S1079898600001931_ref122","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-004-8427-2"},{"key":"S1079898600001931_ref110","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2002.1830"},{"key":"S1079898600001931_ref132","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"S1079898600001931_ref084","unstructured":"Goldreich O. and Zuckerman D. , Another proof the BPP \u2286 PH (and more), Technical Report 45, Electronic Colloquium on Computational Complexity, 1997."},{"key":"S1079898600001931_ref078","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.004"},{"key":"S1079898600001931_ref090","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-06-01126-8"},{"key":"S1079898600001931_ref147","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(97)00029-8"},{"key":"S1079898600001931_ref091","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1109\/ICTAI.2004.115","volume-title":"Proceedings of the sixteenth IEEE conference on tools with artificial intelligence","author":"Huang","year":"2004"},{"key":"S1079898600001931_ref111","volume-title":"Proceedings of IEEE\/ACM internation conference on computer-aided design","author":"Marques-Silva","year":"1996"},{"key":"S1079898600001931_ref113","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-12788-9_6"},{"key":"S1079898600001931_ref134","volume-title":"Metamathematics of first-order arithmetic","author":"Pudl\u00e1k","year":"1993"},{"key":"S1079898600001931_ref161","doi-asserted-by":"publisher","DOI":"10.1137\/0207018"},{"key":"S1079898600001931_ref160","unstructured":"Woods A. , Some problems in logic and number theory, and their connections, Ph.D. thesis, University of Manchester, 1981."},{"key":"S1079898600001931_ref150","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.09.024"},{"key":"S1079898600001931_ref117","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9"},{"key":"S1079898600001931_ref080","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1145\/509907.509985","volume-title":"Proceedings of the thiry-fourth annual ACM symposium on theory of computing","author":"Feige","year":"2002"},{"key":"S1079898600001931_ref158","first-page":"86","article-title":"Space and width in propositional resolution","volume":"83","author":"Tor\u00e1n","year":"2004","journal-title":"Bulletin of the European Association of Theoretical Computer Science"},{"key":"S1079898600001931_ref149","unstructured":"Segerlind N. , New separations in propositional proof complexity, Ph.D. thesis, University of California, San Diego, August 2003."},{"key":"S1079898600001931_ref154","first-page":"600","volume-title":"First international computer science symposium in Russia","author":"Sinz","year":"2006"},{"key":"S1079898600001931_ref118","first-page":"459","volume-title":"Proceedings of the tenth national conference on artificial intelligence","author":"Mitchell","year":"1992"},{"key":"S1079898600001931_ref157","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90029-7"},{"key":"S1079898600001931_ref159","first-page":"425","author":"Urquhart","year":"1995","journal-title":"The complexity of propositional proofs"},{"key":"S1079898600001931_ref148","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0036203"},{"key":"S1079898600001931_ref024","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-61551-2_65","volume-title":"Proceedings of the second international conference on principles and practice of constraint programming","author":"Bayardo","year":"1996"},{"key":"S1079898600001931_ref129","doi-asserted-by":"crossref","DOI":"10.1090\/dimacs\/031\/07","volume-title":"Descriptive complexity and finite models","volume":"31","author":"Pitassi","year":"1997"},{"key":"S1079898600001931_ref005","first-page":"1","volume-title":"Feasible mathematics","volume":"9","author":"Ajtai","year":"1990"},{"key":"S1079898600001931_ref035","first-page":"563","volume-title":"Proceedings of the thirty-fourth annual ACM symposium on theory of computing","author":"Ben-Sasson","year":"2002"},{"key":"S1079898600001931_ref146","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.01.004"},{"key":"S1079898600001931_ref106","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600001931","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T07:53:13Z","timestamp":1684309993000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600001931\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":161,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["S1079898600001931"],"URL":"https:\/\/doi.org\/10.2178\/bsl\/1203350879","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}