{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:46:08Z","timestamp":1725486368252},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429579"},{"type":"electronic","value":"9783540456537"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45653-8_11","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:57:30Z","timestamp":1181350650000},"page":"157-171","source":"Crossref","is-referenced-by-count":0,"title":["Counting the Number of Equivalent Binary Resolution Proofs"],"prefix":"10.1007","author":[{"given":"Joseph D.","family":"Horton","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"key":"11_CR1","unstructured":"R.S. Boyer. Locking: a Restriction of Resolution. PhD thesis, University of Texas at Austin, 1971."},{"key":"11_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York and London, 1973."},{"key":"11_CR3","first-page":"1","volume":"2","author":"H. Nivelle de","year":"1996","unstructured":"Hans de Nivelle. Resolution games and non-liftable resolution orderings. Collegium Logicum, Annals of the Kurt G\u00f6del Society, 2:1\u201320, 1996.","journal-title":"Collegium Logicum, Annals of the Kurt G\u00f6del Society"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1137\/0222044","volume":"22","author":"A. Goerdt","year":"1993","unstructured":"Andreas Goerdt. Regular resolution versus unrestricted resolution. SIAM Journal on Computing, 22:661\u2013683, 1993.","journal-title":"SIAM Journal on Computing"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0004-3702(96)00046-X","volume":"92","author":"J.D. Horton","year":"1997","unstructured":"J.D. Horton and B. Spencer. Clause trees: a tool for understanding and implementing resolution in automatedreasoning. Artificial Intelligence, 92:25\u201389, 1997.","journal-title":"Artificial Intelligence"},{"key":"11_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/BFb0054275","volume-title":"Automated Deduction-CADE-15","author":"J.D. Horton","year":"1998","unstructured":"J.D. Horton and B. Spencer. Rank\/activity: a canonical form for binary resolution.In C. Kirchner and H. Kirchner, editors, Automated Deduction-CADE-15, LNAI 1421:412\u2013426, Lindau, Germany, July 1998. Springer."},{"key":"11_CR7","volume-title":"Seminar notes","author":"J. Reynolds","year":"1965","unstructured":"J. Reynolds. Seminar notes. Stanford University, Palo Alto, California, 1965."},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson. A machine-orientedlogic basedon the resolution principle. J. ACM, 12:23\u201341, 1965.","journal-title":"J. ACM"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01530763","volume":"12","author":"B. Spencer","year":"1994","unstructured":"Bruce Spencer. Avoiding duplicate proofs with the foothold refinement. Annals of Mathematics and Artificial Intelligence, 12:117\u2013140, 1994.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1006241826565","volume":"25","author":"B. Spencer","year":"2000","unstructured":"Bruce Spencer and J.D. Horton. Efficient algorithms to detect andrestore minimality, an extension of the regular restriction of resolution. Journal of Automated Reasoning, 25:1\u201334, 2000.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45653-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T03:24:53Z","timestamp":1550373893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}