{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T18:40:42Z","timestamp":1736016042400,"version":"3.32.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":6,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540115587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0000053","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:26:23Z","timestamp":1128507983000},"page":"85-108","source":"Crossref","is-referenced-by-count":11,"title":["Logic machine architecture: Inference mechanisms"],"prefix":"10.1007","author":[{"given":"Ewing L.","family":"Lusk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ross A","family":"Overbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"W. W. Bledsoe and Larry M. Hines, \u201cVariable elimination and chaining in a resolution-based prover for inequalities,\u201d in Proceedings of the Fifth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (July 1980).","DOI":"10.1007\/3-540-10009-1_7"},{"key":"5_CR2","unstructured":"E. Lusk, William McCune, and R. Overbeek, Logic machine architecture: kernel functions, preprint."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"E. Lusk and R. Overbeek, \u201cData structures and control architecture for the implementation of theorem-proving programs,\u201d in Proceedings of the Fifth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (1980).","DOI":"10.1007\/3-540-10009-1_19"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, R. Overbeek, and L. Wos, \u201cComplexity and related enhancements for automated theorem-proving programs,\u201d Computers and Mathematics with Applications 2 pp. 1\u201316 (1976).","journal-title":"Computers and Mathematics with Applications"},{"key":"5_CR5","unstructured":"William W. McCune, An inference mechanism far resolution-style theorem provers. Master's Thesis, Northwestern University 1981."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0898-1221(75)90019-X","volume":"1","author":"R. Overbeek","year":"1975","unstructured":"R. Overbeek, \u201cAn implementation of hyper-resolution,\u201d Computers and Mathematics with Applications 1 pp. 201\u2013214 (1975).","journal-title":"Computers and Mathematics with Applications"}],"container-title":["Lecture Notes in Computer Science","6th Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000053.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T18:12:44Z","timestamp":1736014364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000053"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540115587"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/bfb0000053","relation":{},"subject":[]}}