{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:32:52Z","timestamp":1725456772468},"publisher-location":"Berlin\/Heidelberg","reference-count":13,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540529535"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0029622","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T05:33:46Z","timestamp":1133415226000},"page":"300-305","source":"Crossref","is-referenced-by-count":2,"title":["Unrestricted resolution versus N-resolution"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Goerdt","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"31_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":"31_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":"31_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."},{"key":"31_CR4","unstructured":"A. Goerdt, Davis Putnam resolution versus unrestricted resolution, Journal of Discrete Applied Mathematics, Special issue on proof lengths, accepted for publication."},{"key":"31_CR5","unstructured":"A. Goerdt, Regular resolution versus unrestricted resolution, Technical report, Univ. of Duisburg, submitted."},{"key":"31_CR6","doi-asserted-by":"crossref","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":"31_CR7","unstructured":"J. A. Robinson, Automatic deduction with hyper-resolution, (1965), in [11] vol. 1, 416\u2013423."},{"key":"31_CR8","volume-title":"Logik f\u00fcr Informatiker, BI-Taschenbuch, Reihe Informatik 56","author":"U. Sch\u00f6ning","year":"1987","unstructured":"U. Sch\u00f6ning, Logik f\u00fcr Informatiker, BI-Taschenbuch, Reihe Informatik 56 (Bibliographisches Institut, Mannheim, 1987)."},{"key":"31_CR9","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0022681","volume":"132","author":"M. E. Stickel","year":"1986","unstructured":"M. E. Stickel, An introduction to automated deduction, Fundamentals of artificial intelligence (Bibel, Jorrand eds.), Lect. Notes of Comp. Sci. 132 (Springer Verlag, Berlin, 1986) 75\u2013137.","journal-title":"Lect. Notes of Comp. Sci."},{"key":"31_CR10","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"M. E. Stickel, A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler, J. of Automated Reasoning 4 (1988) 353\u2013380.","journal-title":"J. of Automated Reasoning"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"J. Siekmann, G. Wrightson (eds.), Automation of reasoning \u2014 classical papers on computational logic, vol.1 and 2, Springer (1983).","DOI":"10.1007\/978-3-642-81955-1"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"G. A. Wilson, C. Minker, Resolution, refinements and search strategies: A comparative study, IEEE Transactions on Computers C-25 (1976).","DOI":"10.1109\/TC.1976.1674697"},{"key":"31_CR13","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. March 34 (1987), 209\u2013219.","journal-title":"J. Assoc. Comput. March"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1990"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0029622","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:15:47Z","timestamp":1586592947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0029622"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540529535"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0029622","relation":{},"subject":[]}}