{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:25:38Z","timestamp":1742977538571,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054275","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"412-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Rank\/activity: A canonical form for binary resolution"],"prefix":"10.1007","author":[{"given":"J. D.","family":"Horton","sequence":"first","affiliation":[]},{"given":"Bruce","family":"Spencer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"36_CR1","first-page":"1259","volume":"3","author":"G. M. Adelson-Velskii","year":"1962","unstructured":"G. M. Adelson-Velskii and E. M. Landis. An algorithm for the organizaton of information. Soviet Math. Doklady, 3:1259\u20131263, 1962.","journal-title":"Soviet Math. Doklady"},{"key":"36_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. 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":"36_CR3","first-page":"1","volume":"2","author":"H. de Nivelle","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":"36_CR4","volume-title":"Technical Report TR97-115","author":"J. D. Horton","year":"1997","unstructured":"J. D. Horton and Bruce Spencer. Bottom up procedures to construct each minimal clause tree once. Technical Report TR97-115, Faculty of Computer Science, University of New Brunwsick, PO Box 4400, Fredericton, New Brunswick, Canada, 1997."},{"key":"36_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 Bruce Spencer. Clause trees: a tool for understanding and implementing resolution in automated reasoning. Artificial Intelligence, 92:25\u201389, 1997.","journal-title":"Artificial Intelligence"},{"key":"36_CR6","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-oriented logic based on the resolution principle. J. ACM, 12:23\u201341, 1965.","journal-title":"J. ACM"},{"key":"36_CR7","unstructured":"Bruce Spencer and J.D. Horton. Extending the regular restriction of resolution to non-linear subdeductions. In Proceedings of the Fourteenth National Conference on Artificial Intelligence, pages 478\u2013483. AAAI Press\/MIT Press, 1997."},{"key":"36_CR8","unstructured":"Bruce Spencer and J.D. Horton. Efficient procedures to detect and restore minimality, an extension of the regular restriction of resolution. Journal of Automated Reasoning, 1998. accepted for publication."},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics, Seminars in Mathematics: Mathematicheskii Institute, pages 115\u2013125. Consultants Bureau, 1969.","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"36_CR10","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, Englewood Cliffs, New Jersey, 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T23:22:17Z","timestamp":1676676137000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0054275","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}