{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T18:40:25Z","timestamp":1736016025813,"version":"3.32.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":8,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540115587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0000052","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:26:23Z","timestamp":1128507983000},"page":"70-84","source":"Crossref","is-referenced-by-count":14,"title":["Logic machine architecture: Kernel functions"],"prefix":"10.1007","author":[{"given":"Ewing L.","family":"Lusk","sequence":"first","affiliation":[]},{"given":"William W.","family":"McCune","sequence":"additional","affiliation":[]},{"given":"Ross A","family":"Overbeek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_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":"4_CR2","volume-title":"Ph.D. Thesis","author":"R. S. Boyer","year":"1971","unstructured":"R. S. Boyer, Locking: a restriction of resolution, Ph.D. Thesis, Univ. of Texas at Austin 1971."},{"key":"4_CR3","unstructured":"Lawrence Henschen, R. Overbeek, and Lawrence Wos, \u201cHyperparamodulation: a refinement of paramodulation,\u201d in Proceedings of the Fifth Conference an Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (July 1960)."},{"key":"4_CR4","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":"4_CR5","unstructured":"E. Lusk and R. Overbeek, Standardizing the external format of formulas, (preprint). September 1980."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"E. Lusk and R. Overbeek, \u201cExperiments with resolution-based theorem-proving algorithms,\u201d Computers and Mathematics with Applications, (1981). (to appear)","DOI":"10.1016\/0898-1221(82)90053-0"},{"key":"4_CR7","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"},{"issue":"8","key":"4_CR8","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1109\/TC.1976.1674702","volume":"25","author":"S. Winker","year":"1976","unstructured":"S. Winker, \u201cAn evaluation of an implementation of qualified hyperresolution,\u201d IEEE Transactions on Computers C-25(8) pp. 835\u2013843 (August 1976).","journal-title":"IEEE Transactions on Computers"}],"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\/BFb0000052.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T18:12:53Z","timestamp":1736014373000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540115587"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0000052","relation":{},"subject":[]}}