{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:25Z","timestamp":1725663505921},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_213","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:28Z","timestamp":1330251748000},"page":"731-734","source":"Crossref","is-referenced-by-count":5,"title":["ROO: A parallel theorem prover"],"prefix":"10.1007","author":[{"given":"Ewing L.","family":"Lusk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William W.","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Slaney","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"63_CR1","volume-title":"Technical Report ANL-91\/15","author":"V. Herrarte","year":"1991","unstructured":"Virginia Herrarte and Ewing Lusk. Studying parallel program behavior with upshot. Technical Report ANL-91\/15, Argonne National Laboratory, Argonne, IL 60439, 1991."},{"key":"63_CR2","doi-asserted-by":"crossref","unstructured":"Ewing L. Lusk and William W. McCune. Experiments with Roo, a parallel automated deduction system. (To appear in Springer Lecture Notes in Artificial Intelligence), 1992.","DOI":"10.1007\/3-540-55425-4_6"},{"key":"63_CR3","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Single axioms in the implicational prepositional calculus. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science 310, pages 710\u2013713. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012869"},{"key":"63_CR4","doi-asserted-by":"crossref","unstructured":"John K. Slaney and Ewing L. Lusk. Parallelizing the closure operation in automated deduction. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 449, pages 28\u201339. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_77"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_213.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:00:27Z","timestamp":1605646827000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_213","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}