{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:53:13Z","timestamp":1725663193136},"publisher-location":"Berlin, Heidelberg","reference-count":10,"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_143","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T14:01:47Z","timestamp":1330178507000},"page":"697-698","source":"Crossref","is-referenced-by-count":5,"title":["ITP at argonne national laboratory"],"prefix":"10.1007","author":[{"given":"Ewing","family":"Lusk","sequence":"first","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":"69_CR1","unstructured":"Charles H. Applebaum, Logic Machine Architecture Database Support System: Layer 1 User's Manual, The MITRE Corporation, Bedford, MA (November, 1985)."},{"key":"69_CR2","doi-asserted-by":"crossref","unstructured":"Ralph Butler, Ewing Lusk, William McCune, and Ross Overbeek, \u201cPaths to High Performance Automated Theorem Proving,\u201d CADE-8 (July, 1986).","DOI":"10.1007\/3-540-16780-3_123"},{"key":"69_CR3","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":"69_CR4","series-title":"Springer-Verlag Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BFb0000053","volume-title":"Proceedings of the Sixth Conference on Automated Deduction","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":"69_CR5","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":"69_CR6","unstructured":"Ewing L. Lusk and Ross A. Overbeek, \u201cLogic Machine Architecture inference mechanisms \u2014 layer 2 user reference manual-Release 2.0,\u201d ANL-82-84, Argonne National Laboratory (April, 1984)."},{"key":"69_CR7","unstructured":"Ewing L. Lusk and Ross A. Overbeek, \u201cThe automated reasoning system ITP,\u201d ANL-84-27, Argonne National Laboratory (April, 1984)."},{"key":"69_CR8","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"},{"key":"69_CR9","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 (1981).","DOI":"10.1145\/1500412.1500517"},{"key":"69_CR10","unstructured":"L. Wos, R. Veroff, B. Smith, and W. McCune, \u201cThe Linked Inference Principle, II: The User's Viewpoint,\u201d 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"}],"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_143.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:11:39Z","timestamp":1605625899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_143"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_143","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}