{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:28Z","timestamp":1725663868327},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540527534"},{"type":"electronic","value":"9783540471370"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52753-2_37","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:42:33Z","timestamp":1330188153000},"page":"143-162","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Davis-Putnam resolution versus unrestricted resolution"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Goerdt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"M. Ajtai, The complexity of the propositional pigeonhole principle, Proc. of the IEEE FOCS (1988).","DOI":"10.1109\/SFCS.1988.21951"},{"key":"9_CR2","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(88)90072-2","volume":"62","author":"S. R. Buss","year":"1988","unstructured":"S. R. Buss and G. Tur\u00e1n, Resolution proofs of generalized pigeonhole principles, Theoret. Comp. Sci. 62 (1988) 311\u2013317.","journal-title":"Theoret. Comp. Sci."},{"issue":"4","key":"9_CR3","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"V. Chv\u00e1tal and E. Szemeredi, Many hard examples for resolution, J. Assoc. Comput. Mach. 35 (4) (1988) 759\u2013768.","journal-title":"J. Assoc. Comput. Mach."},{"issue":"1","key":"9_CR4","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"S. A. Cook","year":"1979","unstructured":"S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44(1) (1979) 36\u201350.","journal-title":"J. Symbolic Logic"},{"key":"9_CR5","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, JACM 7 (1960) 201\u2013215.","journal-title":"JACM"},{"key":"9_CR6","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0304-3975(77)90054-8","volume":"4","author":"Z. Galil","year":"1977","unstructured":"Z. Galil, On the complexity of regular resolution and the Davis-Putnam procedure, Theoret. Comput. Sci. 4 (1977) 23\u201346.","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR7","unstructured":"A. Goerdt, Unrestricted resolution versus N-resolution, Technical report, Universit\u00e4t-GH-Duisburg (1989) submitted."},{"key":"9_CR8","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 of resolution, Theoret. Comput. Sci 39 (1985) 297\u2013308.","journal-title":"Theoret. Comput. Sci"},{"key":"9_CR9","unstructured":"R. A. Reckhow, On the lengths of proofs in the propositional calculus, Ph. D. thesis, University of Toronto (1975)."},{"key":"9_CR10","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"A. Urquhart, Hard examples for resolution, J. Assoc. Comput. Mach. 34 (1987) 209\u2013219.","journal-title":"J. Assoc. Comput. Mach."}],"container-title":["Lecture Notes in Computer Science","CSL '89"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52753-2_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:43:53Z","timestamp":1558255433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52753-2_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540527534","9783540471370"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-52753-2_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}