{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T10:40:01Z","timestamp":1736592001699,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540659228"},{"type":"electronic","value":"9783540488552"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10703163_12","type":"book-chapter","created":{"date-parts":[[2006,10,9]],"date-time":"2006-10-09T18:15:50Z","timestamp":1160417750000},"page":"171-178","source":"Crossref","is-referenced-by-count":4,"title":["An Upper Bound for Minimal Resolution Refutations"],"prefix":"10.1007","author":[{"given":"Hans Kleine","family":"B\u00fcning","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1016\/0097-3165(86)90060-9","volume":"43","author":"R. Aharoni","year":"1986","unstructured":"Aharoni, R., Linial, N.: Minimal Non\u2013Two\u2013Colorable Hypergraphs and Minimal Unsatisfiable Formulas. Journal of Combinatorial Theory\u00a043, 196\u2013204 (1986)","journal-title":"Journal of Combinatorial Theory"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Beame, P., Pitassi, T.: Simplified and Improved Resolution Lower Bounds. In: FOCS 1996, pp. 274\u2013282 (1996)","DOI":"10.1109\/SFCS.1996.548486"},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chvatal","year":"1988","unstructured":"Chvatal, V., Szemeredi, T.: Many hard Exanples for Resolution. Journal of the Association for Computing Maschinery\u00a035, 759\u2013768 (1988)","journal-title":"Journal of the Association for Computing Maschinery"},{"key":"12_CR4","unstructured":"Davydov, G., Davydova, I., Kleine B\u00fcning, H.: An Effcient Algorithm for the Minimal Unsatisfiability Problem for a Subclass of CNF. To appear in Annals of Mathematics and Artificial Intelligence"},{"key":"12_CR5","unstructured":"Fu, X.: On the Complexity of Proof Systems. University of Toronto, PhD Thesis (1995)"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractibility of Resolution. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard Examples for Resolution. Journal of ACM\u00a034, 209\u2013219 (1987)","journal-title":"Journal of ACM"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703163_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T09:38:39Z","timestamp":1736588319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703163_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540659228","9783540488552"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/10703163_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}