{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:02Z","timestamp":1749124082532},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540554257"},{"type":"electronic","value":"9783540470663"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55425-4_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:59:11Z","timestamp":1330250351000},"page":"139-162","source":"Crossref","is-referenced-by-count":20,"title":["Experiments with Roo, a parallel automated deduction system"],"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"}]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. Bledsoe","year":"1990","unstructured":"W. Bledsoe. Challenge problems in elementary calculus. Journal of Automated Reasoning, 6(3):341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR2","first-page":"551","volume-title":"Lecture Notes in Computer Science, Vol. 355","author":"J. Christian","year":"1989","unstructured":"J. Christian. Fast Knuth-Bendix completion: A summary. In N. Dershowitz, editor, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 355, pages 551\u2013555, New York, 1989. Springer-Verlag."},{"issue":"1","key":"6_CR3","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J. Guard","year":"1969","unstructured":"J. Guard, F. Oglesby, J. Bennett, and L. Settle. Semi-automated mathematics. Journal of the ACM, 16(1):49\u201362, 1969.","journal-title":"Journal of the ACM"},{"issue":"14","key":"6_CR4","first-page":"193","volume":"2","author":"J. A. Kalman","year":"1975","unstructured":"J. A. Kalman. Axiomatizations of logics with values in groups. Journal of the London Math. Society, 2(14):193\u2013199, 1975.","journal-title":"Journal of the London Math. Society"},{"key":"6_CR5","unstructured":"J. Lukasiewicz. Selected Works. North-Holland, 1970. Edited by L. Borkowski."},{"key":"6_CR6","first-page":"85","volume-title":"Lecture Notes in Computer Science, Vol. 138","author":"E. Lusk","year":"1982","unstructured":"E. Lusk, W. McCune, and R. Overbeek. Logic Machine Architecture: Inference mechanisms. In D. Loveland, editor, Proceedings of the 6th Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages 85\u2013108, New York, 1982. Springer-Verlag."},{"key":"6_CR7","first-page":"70","volume-title":"Lecture Notes in Computer Science, Vol. 138","author":"E. Lusk","year":"1982","unstructured":"E. Lusk, W. McCune, and R. Overbeek. Logic Machine Architecture: Kernel functions. In D. Loveland, editor, Proceedings of the 6th Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 138, pages 70\u201384, New York, 1982. Springer-Verlag."},{"key":"6_CR8","volume-title":"High-performance parallel theorem proving for shared-memory multiprocessors","author":"E. Lusk","year":"1991","unstructured":"E. Lusk, W. McCune, and J. Slaney. High-performance parallel theorem proving for shared-memory multiprocessors. Preprint, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. In preparation."},{"key":"6_CR9","volume-title":"ROO\u2014a parallel theorem prover. Tech. Memo. MCS-TM-149","author":"E. Lusk","year":"1991","unstructured":"E. Lusk, W. McCune, and J. Slaney. ROO\u2014a parallel theorem prover. Tech. Memo. MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. To appear."},{"issue":"1","key":"6_CR10","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF02575007","volume":"36","author":"E. Lusk","year":"1987","unstructured":"E. Lusk and R. McFadden. Using automated reasoning tools: A study of the semigroup F2B2. Semigroup Forum, 36(1):75\u201388, 1987.","journal-title":"Semigroup Forum"},{"key":"6_CR11","volume-title":"Tech. Report ANL-84\/27","author":"E. Lusk","year":"1984","unstructured":"E. Lusk and R. Overbeek. The automated reasoning system ITP. Tech. Report ANL-84\/27, Argonne National Laboratory, Argonne, IL, April 1984."},{"key":"6_CR12","volume-title":"Tech. Report ANL-90\/9","author":"W. McCune","year":"1990","unstructured":"W. McCune. otter 2.0 Users Guide. Tech. Report ANL-90\/9, Argonne National Laboratory, Argonne, IL, March 1990."},{"key":"6_CR13","volume-title":"Preprint MCS-P219-0391","author":"W. McCune","year":"1991","unstructured":"W. McCune. Single axioms for the left group and right group calculi. Preprint MCS-P219-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991."},{"key":"6_CR14","volume-title":"Tech. Memo. ANL\/MCS-TM-153","author":"W. McCune","year":"1991","unstructured":"W. McCune. What's new in otter 2.2. Tech. Memo. ANL\/MCS-TM-153, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, July 1991."},{"key":"6_CR15","first-page":"710","volume-title":"Lecture Notes in Computer Science, Vol. 310","author":"F. Pfenning","year":"1988","unstructured":"F. Pfenning. Single axioms in the implicational propositional calculus. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 310, pages 710\u2013713, New York, 1988. Springer-Verlag."},{"issue":"1","key":"6_CR16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF03023980","volume":"12","author":"L. Sallows","year":"1990","unstructured":"L. Sallows. A curious new result in switching theory. The Mathematical Intelligencer, 12(1):21\u201332, 1990.","journal-title":"The Mathematical Intelligencer"},{"key":"6_CR17","first-page":"40","volume-title":"Lecture Notes in Artificial Intelligence, Vol. 449","author":"J. Schumann","year":"1990","unstructured":"J. Schumann and R. Letz. PARTHEO: A high-performance parallel theorem prover. In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 40\u201356, New York, July 1990. Springer-Verlag."},{"key":"6_CR18","first-page":"28","volume-title":"Lecture Notes in Artificial Intelligence, Vol. 449","author":"J. Slaney","year":"1990","unstructured":"J. Slaney and E. Lusk. Parallelizing the closure computation in automated deduction. In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 28\u201339, New York, July 1990. Springer-Verlag."},{"issue":"4","key":"6_CR19","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1988","unstructured":"M. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4(4):353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"6_CR20","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00244359","volume":"6","author":"S. Winker","year":"1990","unstructured":"S. Winker. Robbins algebra: Conditions that make a near-boolean algebra boolean. Journal of Automated Reasoning, 6(4):465\u2013489, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR21","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. Prentice-Hall, Englewood Cliffs, NJ, 1984."},{"issue":"4","key":"6_CR22","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM, 12(4):536\u2013541, 1965.","journal-title":"J. ACM"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"L. Wos, S. Winker, and E. Lusk. An automated reasoning system. In Proceedings of the National Computer Conference, pages 697\u2013702. AFIPS, 1981.","DOI":"10.1145\/1500412.1500517"}],"container-title":["Lecture Notes in Computer Science","Parallelization in Inference Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55425-4_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:31:05Z","timestamp":1619573465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55425-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540554257","9783540470663"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-55425-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}