{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T15:26:07Z","timestamp":1725636367265},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540531326"},{"type":"electronic","value":"9783642760716"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/978-3-642-76071-6_20","type":"book-chapter","created":{"date-parts":[[2011,11,22]],"date-time":"2011-11-22T18:16:55Z","timestamp":1321985815000},"page":"181-185","source":"Crossref","is-referenced-by-count":2,"title":["Comparing the Complexity of Regular and Unrestricted Resolution"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Goerdt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","volume-title":"The complexity of the propositional pigeonhole principle","author":"M Ajtai","year":"1988","unstructured":"M. Ajtai, The complexity of the propositional pigeonhole principle, Proc. of the IEEE FOCS (1988)."},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0004-3702(82)90024-8","volume":"18","author":"W Bibel","year":"1982","unstructured":"W. Bibel, A comparative study of several proof procedures, Artificial Intelligence 18 (1982) 269\u2013293.","journal-title":"Artificial Intelligence"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(88)90072-2","volume":"62","author":"SR Buss","year":"1988","unstructured":"S.R. Buss and G. Turan, Resolution proofs of generalized pigeonhole principles, Theoret. Comp. Sci. 62 (1988) 311\u2013317.","journal-title":"Comp. Sci"},{"issue":"4","key":"20_CR4","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":"Many hard examples for resolution,J Assoc.comput.mach"},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA 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":"20_CR6","volume-title":"Relative complexities of first order calculi","author":"E Eder","year":"1990","unstructured":"E. Eder, Relative complexities of first order calculi, Habilitationsschrift, University of Dortmund (1990)."},{"issue":"1","key":"20_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/0167-4048(85)90006-9","volume":"4","author":"Z Galil","year":"1977","unstructured":"Z. Galil, On the complexity of regular resolution and the Davis-Putman procedure, Theoret. Comput. Sei. 4(1) (1977) 23\u201346.","journal-title":"Comput.Sei"},{"doi-asserted-by":"crossref","unstructured":"A. Goerdt, Unrestricted resolution versus N-resolution, Proc. MFCS 1990, LNCS, accepted for publication.","key":"20_CR8","DOI":"10.1007\/BFb0029622"},{"unstructured":"9.Goerdt, Davis-Putmann resolution versus unrestricted resolution, Journal of Discrete Applied Mathematics, Special issue on proof lengths, accepted for publication.","key":"20_CR9"},{"doi-asserted-by":"crossref","unstructured":"A. Goerdt, Regular resolution versus unrestricted resolution, Technical report, University of Duisburg (1990) submitted.","key":"20_CR10","DOI":"10.1007\/3-540-52753-2_37"},{"key":"20_CR11","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. Comp. Sci. 39 (1985), 297\u2013308.","journal-title":"Comp. Sci"},{"key":"20_CR12","volume-title":"(North Holland","author":"DW Loveland","year":"1978","unstructured":"D.W. Loveland, Automated Theorem proving: a logical basis, (North Holland 1978)."},{"key":"20_CR13","volume-title":"Reihe Informatik","author":"U Sch\u00f6ning","year":"1987","unstructured":"U. Sch\u00f6ning, Logik f\u00fcr Informatiker, BI-Taschenbuch, Reihe Informatik 56 (Bibliographisches Institut, Mannheim, 1987)."},{"volume-title":"Automation of reasoning-classical papers on computational logic","year":"1983","unstructured":"J. Siekmann and G. Wrightson (eds.), Automation of reasoning-classical papers on computational logic, vol. 1 and 2 (Springer 1983).","key":"20_CR14"},{"key":"20_CR15","first-page":"466","volume":"2","author":"GS Tseitin","year":"1970","unstructured":"GS Tseitin, On the complexity of derivation in the propositional calculus (1970) in [13] vol. 2, 466\u2013486.","journal-title":"calculus"},{"key":"20_CR16","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"},{"key":"20_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(89)90147-3","volume":"66","author":"A Urquhart","year":"1989","unstructured":"A. Urquhart, The complexity of Gentzen Systems for propositional logic, Theoret. Comp. Sci. 66 (1989) 87\u201397.","journal-title":"Comp. Sci"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"25","author":"GA Wilson","year":"1976","unstructured":"G.A. Wilson and C. Minker, Resolution, refinements, and search strategies: A comparative study, IEEE Transactions on Computers C-25 (1976) 782\u2013801.","journal-title":"IEEE Transactions on Computers C-"}],"container-title":["Informatik-Fachberichte","GWAI-90 14th German Workshop on Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-76071-6_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T17:20:11Z","timestamp":1639761611000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-76071-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540531326","9783642760716"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-76071-6_20","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1990]]}}}