{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:52Z","timestamp":1725475792773},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_29","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"385-400","source":"Crossref","is-referenced-by-count":0,"title":["Support Ordered Resolution"],"prefix":"10.1007","author":[{"given":"Bruce","family":"Spencer","sequence":"first","affiliation":[]},{"given":"Joseph D.","family":"Horton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Boyer, R.S.: Locking: A Restriction of Resolution. PhD thesis, University of Texas at Austin (1971)"},{"key":"29_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving.","author":"C.-L. Chang","year":"1973","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)"},{"key":"29_CR3","first-page":"1","volume":"2","author":"H. Nivelle de","year":"1996","unstructured":"de Nivelle, H.: Resolution games and non-liftable resolution orderings. Collegium Logicum, Annals of the Kurt G\u00f6del Society\u00a02, 1\u201320 (1996)","journal-title":"Collegium Logicum, Annals of the Kurt G\u00f6del Society"},{"key":"29_CR4","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0004-3702(96)00046-X","volume":"92","author":"J.D. Horton","year":"1997","unstructured":"Horton, J.D., Spencer, B.: Clause trees: a tool for understanding and implementing resolution in automated reasoning. Artificial Intelligence\u00a092, 25\u201389 (1997)","journal-title":"Artificial Intelligence"},{"key":"29_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/BFb0054275","volume-title":"Automated Deduction - CADE-15","author":"J.D. Horton","year":"1998","unstructured":"Horton, J.D., Spencer, B.: Rank\/activity: a canonical form for binary resolution. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 412\u2013426. Springer, Heidelberg (1998)"},{"key":"29_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM\u00a012, 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"29_CR7","unstructured":"Spencer, B., Horton, J.D.: Efficient procedures for detecting and restoring minimality, an extension of the regular restriction of resolution. Journal of Automated Reasoning (to appear)"},{"key":"29_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Kapur, D. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 252\u2013266. Springer, Heidelberg (1994)"},{"key":"29_CR9","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","volume":"24","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: The CADE-16 system competition. Journal of Automated Reasoning\u00a024, 371\u2013396 (2000)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T06:30:09Z","timestamp":1553322609000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/10721959_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}