{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:26:49Z","timestamp":1725456409915},"publisher-location":"Berlin\/Heidelberg","reference-count":32,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055727X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013052","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:02:07Z","timestamp":1132729327000},"page":"96-106","source":"Crossref","is-referenced-by-count":11,"title":["Controlling redundancy in large search spaces: Argonne-style theorem proving through the years"],"prefix":"10.1007","author":[{"given":"Ewing L.","family":"Lusk","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"Tech. Report ANL-90\/30","author":"R. Butler","year":"1990","unstructured":"R. Butler and R. Overbeek. A tutorial on the construction of high-performance resolution\/paramodulation systems. Tech. Report ANL-90\/30, Argonne National Laboratory, Argonne, IL, 1990."},{"key":"9_CR2","volume-title":"Tech. Memo ANL\/MCS-TM-141","author":"T. Henry","year":"1990","unstructured":"T. Henry and W. McCune. FormEd: An X Window System application for managing first-order formulas. Tech. Memo ANL\/MCS-TM-141, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, October 1990."},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF00263447","volume":"8","author":"A. Jindal","year":"1992","unstructured":"A. Jindal, R. Overbeek, and W. Cabot. Exploitation of parallel processing for implementing high-performance deduction systems. Journal of Automated Reasoning, 8(1):23\u201338, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR4","unstructured":"John Kalman. An itp workbook. Technical Report ANL-86-56, Argonne National Laboratory, December 1986."},{"key":"9_CR5","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebras. Pergamon Press, 1970."},{"key":"9_CR6","volume-title":"Preprint MCS-P254-0791","author":"E. Lusk","year":"1991","unstructured":"E. Lusk and W. McCune. Experiments with Roo, a parallel automated deduction system. Preprint MCS-P254-0791, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. To appear in Springer-Verlag Lecture Notes in Artificial Intelligence."},{"key":"9_CR7","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":"9_CR8","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":"9_CR9","volume-title":"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."},{"issue":"3","key":"9_CR10","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0898-1221(82)90053-0","volume":"8","author":"E. Lusk","year":"1982","unstructured":"E. Lusk and R. Overbeek. Experiments with resolution-based theorem-proving algorithms. Computers and Mathematics with Application, 8(3):141\u2013152, 1982.","journal-title":"Computers and Mathematics with Application"},{"key":"9_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."},{"issue":"1","key":"9_CR12","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"},{"issue":"8","key":"9_CR13","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"25","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, R. Overbeek, and L. Wos. Problems and experiments for and with automated theorem-proving programs. IEEE Transactions on Computers, C-25(8):773\u2013782, August 1976.","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR14","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":"9_CR15","volume-title":"Preprint MCS-P220-0391","author":"W. McCune","year":"1991","unstructured":"W. McCune. Automated discovery of new axiomatizations of the left group and right group calculi. Preprint MCS-P220-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. To appear in J. Automated Reasoning."},{"key":"9_CR16","volume-title":"Preprint MCS-P191-1190","author":"W. McCune","year":"1991","unstructured":"W. McCune. Experiments with discrimination tree indexing and path indexing for term retrieval. Preprint MCS-P191-1190, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991. Invited paper, to appear in J. of Automated Reasoning."},{"key":"9_CR17","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":"9_CR18","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":"9_CR19","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0304-3975(91)90034-Y","volume":"87","author":"W. McCune","year":"1991","unstructured":"W. McCune and L. Wos. The absence and the presence of fixed point combinators. Theoretical Computer Science, 87:221\u2013228, 1991.","journal-title":"Theoretical Computer Science"},{"key":"9_CR20","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/321812.321814","volume":"21","author":"R. Overbeek","year":"1974","unstructured":"R. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21:191\u2013200, 1974.","journal-title":"Journal of the ACM"},{"key":"9_CR21","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. An implementation of hyper-resolution. Computers and Mathematics with Applications, 1:201\u2013214, 1975.","journal-title":"Computers and Mathematics with Applications"},{"key":"9_CR22","unstructured":"G. Robinson and L. Wos. Paramodulation and theorem-proving in first-order theories with equality. In D. Michie and R. Meltzer, editors, Machine Intelligence, Vol. IV, pages 135\u2013150. Edinburg U. Press, 1969."},{"key":"9_CR23","volume-title":"Tech. Report TR-ARP-10\/91","author":"J. Slaney","year":"1991","unstructured":"J. Slaney. Finder, finite domain enumerator: Version 1.0 notes and guide. Tech. Report TR-ARP-10\/91, Automated Reasoning Project, Australian National University, Canberra, Australia, 1991."},{"key":"9_CR24","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."},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"S. Winker. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. J. ACM, 29:273\u2013284, 1982.","journal-title":"J. ACM"},{"key":"9_CR26","first-page":"533","volume":"37","author":"S. Winker","year":"1981","unstructured":"S. Winker, L. Wos, and E. Lusk. Semigroups, antiautomorphisms, and involutions: A computer solution to an open problem, I. Math. of Comp., 37:533\u2013545, 1981.","journal-title":"Math. of Comp."},{"key":"9_CR27","first-page":"615","volume-title":"Proceedings of the Fall Joint Computer Conferenc","author":"L. Wos","year":"1964","unstructured":"L. Wos, D. Carson, and G. Robinson. The unit preference strategy in theorem proving. In Proceedings of the Fall Joint Computer Conferenc, pages 615\u201362, New York, 1964. Thompson Book Compan."},{"key":"9_CR28","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. McGraw-Hill, second edition, 1992."},{"issue":"4","key":"9_CR29","doi-asserted-by":"publisher","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":"9_CR30","doi-asserted-by":"crossref","unstructured":"L. Wos, S. Winker, and E. Lusk. An automated reasoning system. In Proceedings of the AFIPS National Computer Conference, pages 697\u2013702, 1981.","DOI":"10.1145\/1500412.1500517"},{"key":"9_CR31","first-page":"485","volume-title":"Lecture Notes in Artificial Intelligence, Vol. 449","author":"L. Wos","year":"1990","unstructured":"L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler. Automated reasoning contributes to mathematics and logic. In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 485\u2013499, New York, July 1990. Springer-Verlag."},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0004-3702(84)90054-7","volume":"22","author":"L. Wos","year":"1984","unstructured":"L. Wos, S, Winker, B. Smith, R. Veroff, and L. Henschen. A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains. Artificial Intelligence, 22:303\u2013356, 1984.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0013052.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:53Z","timestamp":1607353613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055727X"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/bfb0013052","relation":{},"subject":[]}}