{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T22:27:37Z","timestamp":1762295257938},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_123","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:00:15Z","timestamp":1330196415000},"page":"588-597","source":"Crossref","is-referenced-by-count":8,"title":["Paths to high-performance automated theorem proving"],"prefix":"10.1007","author":[{"given":"Ralph","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewing","family":"Lusk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ross","family":"Overbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"49_CR1","series-title":"Technical Report","volume-title":"A tutorial on the Warren abstract machine","author":"J. Gabriel","year":"1984","unstructured":"J. Gabriel, T. Lindholm, E. Lusk, and R. A. Overbeek, \u201cA tutorial on the Warren abstract machine,\u201d Technical Report ANL-84-84, Argonne National Laboratory, Argonne, Illinois (October, 1984)."},{"key":"49_CR2","unstructured":"J. Gabriel, T. Lindholm, E. L. Lusk, and R. A. Overbeek, \u201cLogic Programming on the HEP,\u201d in Parallel MIMD Computation: The HEP Supercomputer and its Applications, ed. J. S. Kowalik, The MIT Press (1985)."},{"key":"49_CR3","volume-title":"Design, application and implementation of a parallel logic programming language","author":"S. Gregory","year":"1985","unstructured":"Steven Gregory, Design, application and implementation of a parallel logic programming language, Doctoral Thesis, Imperial College of Science and Technology, London, September 1985."},{"key":"49_CR4","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/BFb0000052","volume-title":"Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138","author":"E. Lusk","year":"1982","unstructured":"E. Lusk, William McCune, and R. Overbeek, \u201cLogic machine architecture: kernel functions,\u201d pp. 70\u201384 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland, Springer-Verlag, New York (1982)."},{"key":"49_CR5","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BFb0000053","volume-title":"Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138","author":"E. Lusk","year":"1982","unstructured":"E. Lusk, William McCune, and R. Overbeek, \u201cLogic machine architecture: inference mechanisms,\u201d pp. 85\u2013108 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland, Springer-Verlag, New York (1982)."},{"key":"49_CR6","series-title":"Technical Report","volume-title":"Implementation of Monitors with Macros: A Programming Aid for the HEP and Other Parallel Processors","author":"E. L. Lusk","year":"1983","unstructured":"Ewing L. Lusk and Ross A. Overbeek, \u201cImplementation of Monitors with Macros: A Programming Aid for the HEP and Other Parallel Processors,\u201d Technical Report ANL-83-97, Argonne National Laboratory, Argonne, Illinois (December 1983)."},{"key":"49_CR7","first-page":"43","volume-title":"Proceedings of the 7th International Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 170","author":"E. L. Lusk","year":"1984","unstructured":"Ewing L. Lusk and Ross A. Overbeek, \u201cA Portable Environment for Research in Automated Reasoning,\u201d pp. 43\u201352 in Proceedings of the 7th International Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 170, ed. R. E. Shostak, Springer-Verlag, New York (1984)."},{"key":"49_CR8","unstructured":"E. L. Lusk, R. L. Stevens, and R. A. Overbeek, \u201cA tutorial on the use of monitors in C: writing portable code for multiprocessors,\u201d ANL-85-2, Argonne National Laboratory (January 1985)."},{"issue":"8","key":"49_CR9","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, R. Overbeek, and L. Wos, \u201cProblems and experiments for and with automated theoremproving programs,\u201d IEEE Transactions on Computers\nC-25(8), pp. 773\u2013782 (1976).","journal-title":"IEEE Transactions on Computers"},{"key":"49_CR10","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\n1, pp. 201\u2013214 (1975).","journal-title":"Computers and Mathematics with Applications"},{"key":"49_CR11","unstructured":"D. H. D. Warren, \u201cImplementing Prolog \u2014 compiling predicate logic programs,\u201d DAI Research Reports 39 and 40, University of Edinburgh (May 1977)."},{"key":"49_CR12","unstructured":"D. H. D. Warren, \u201cAn Abstract Prolog Instruction Set,\u201d SRI Technical Note 309, SRI International (October 1983)."},{"key":"49_CR13","unstructured":"D. H. D. Warren, \u201cApplied logic \u2014 its use and implementation as a programming tool,\u201d SRI International Technical Note 290 (June 1983). University of Edinburgh Ph.D. thesis, 1977"},{"key":"49_CR14","unstructured":"M. J. Wise and D. M. W. Powers, \u201cIndexing Prolog Clauses via Superimposed Code Words and Field Encoded Words,\u201d Proceedings of the 1984 International Symposium on Logic Programming, Atlantic City, pp. 203\u2013211 (February, 1984)."},{"key":"49_CR15","doi-asserted-by":"crossref","unstructured":"L. Wos, S. Winker, and E. Lusk, \u201cAn automated reasoning system,\u201d Proceedings of the AFIPS National Computer Conference, pp. 697\u2013702","DOI":"10.1145\/1500412.1500517"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_123.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:07:04Z","timestamp":1619557624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_123","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}