{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T05:56:19Z","timestamp":1768802179186,"version":"3.49.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881910","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T20:34:58Z","timestamp":1104006898000},"page":"1-33","source":"Crossref","is-referenced-by-count":16,"title":["Parallelization of deduction strategies: An analytical study"],"prefix":"10.1007","volume":"13","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jieh","family":"Hsiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"Anantharaman, S. and Hsiang, J.: Automated proofs of the Moufang identities in alternative rings,Journal of Automated Reasoning 6 (1990), 76?109.","journal-title":"Journal of Automated Reasoning"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Anantharaman, S. and Andrianarivelo, N.: Heuristical criteria in refutational theorem proving, in A. Miola (ed.),Proceedings of the Symposium on the Design and Implementation of Systems for Symbolic Computation, Capri, Italy, 1990, Springer-Verlag, Lecture Notes in Computer Science 429, 1990, pp. 184?193.","DOI":"10.1007\/3-540-52531-9_138"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Loveland, D. W.: METEORs: High performance theorem provers using model elimination, in R. S. Boyer (ed.),Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-94-011-3488-0_2"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Avenhaus, J. and Denzinger, J.: Distributing equational theorem proving, in C. Kirchner (ed.),Proc. 5th Conf. on Rewriting Techniques and Applications, Montreal, Canada, 1993, Springer-Verlag, Lecture Notes in Computer Science 690, 1993, pp. 62?76.","DOI":"10.1007\/3-540-56868-9_6"},{"key":"CR5","unstructured":"Bachmair, L., Dershowitz, N. and Hsiang, J.: Orderings for equational proofs, inProc. 1st Annual IEEE Symp. on Logic in Computer Science, Cambridge, Massachussets, 1986, pp. 346?357."},{"key":"CR6","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures, Vol. II","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N. and Plaisted, D. A.: Completion without failure, in H. Ait-Kaci and M. Nivat (eds.),Resolution of Equations in Algebraic Structures, Vol. II: Rewriting Techniques, Academic Press, New York, 1989, pp. 1?30."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Bachmair, L. and Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria, inProceedings of Logic Programming and Automated Reasoning, Springer-Verlag, Lecture Notes in Artificial Intelligence 624, 1992, pp. 273?284.","DOI":"10.1007\/BFb0013068"},{"key":"CR8","unstructured":"Bonacina, M. P. and Hsiang, J.: On fairness in distributed deduction, in P. Enjalbert, A. Finkel and K. W. Wagner (eds.),Proc. 10th Symp. on Theoretical Aspects of Computer Science, W\u00fcrzburg, Germany, February 1993, Springer-Verlag, Lecture Notes in Computer Science 665, 1993, pp. 141?152."},{"key":"CR9","unstructured":"Bonacina, M. P. and Hsiang, J.: The clause-diffusion methodology for distributed deduction, (preprint)."},{"key":"CR10","unstructured":"Bonacina, M. P.: Distributed Automated Deduction, Ph.D. Thesis, Department of Computer Science, State University of New York at Stony Brook, 1992."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P. and Hsiang, J.: Distributed deduction by clause-diffusion: The Aquarius prover, in A. Miola (ed.),Proc. 3rd Int. Symp. on Design and Implementation of Symbolic Computation Systems, Gmunden, Austria, 1993, Springer-Verlag, Lecture Notes in Computer Science 722, 1993, pp. 272?287.","DOI":"10.1007\/BFb0013183"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF00244281","volume":"8","author":"S. Bose","year":"1992","unstructured":"Bose, S., Clarke, E. M., Long, D. E. and Michaylov, S.: Parthenon: A parallel theorem prover for non-Horn clauses,Journal of Automated Reasoning 8 (1992), 153?182.","journal-title":"Journal of Automated Reasoning"},{"key":"CR13","volume-title":"A Computational Logic","author":"R. Boyer","year":"1979","unstructured":"Boyer, R. and Moore, J. S.:A Computational Logic, Academic Press, New York, 1979."},{"key":"CR14","volume-title":"An Algorithm for Finding a Basis for the Residue Class Ring of a Zerodimensional Polynomial Ideal","author":"B. Buchberger","year":"1965","unstructured":"Buchberger, B.: An Algorithm for Finding a Basis for the Residue Class Ring of a Zerodimensional Polynomial Ideal (in German), Ph.D. Thesis, Department of Mathematics, University of Innsbruck, Austria, 1965."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"Buchberger, B.: History and basic features of the critical-pair\/completion procedure,Journal of Symbolic Computation 3 (1987), 3?38.","journal-title":"Journal of Symbolic Computation"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Chakrabarti, S. and Yelick, K. A.: Implementing an irregular application on a distributed memory multiprocessor, inPrinciples and Practice of Parallel Programming, 1993.","DOI":"10.1145\/155332.155350"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Chakrabarti, S. and Yelick, K. A.: On the correctness of a distributed memory Gr\u00f6bner basis algorithm, in C. Kirchner (ed.),Proc. 5th Conf. on Rewriting Techniques and Applications, Montreal, Canada, 1993, Springer-Verlag, Lecture Notes in Computer Science 690, 1993, 77?91.","DOI":"10.1007\/3-540-56868-9_7"},{"key":"CR18","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, R. C.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"CR19","unstructured":"Cheng, P. D. and Juang, J. Y.: A parallel resolution procedure based on connection graph, inProc. 7th Conf. of the American Association for Artificial Intelligence, 1987, pp. 13?17."},{"key":"CR20","unstructured":"Chou, S. C.: Proving and discovering theorems in elementary geometries using Wu's method, Ph.D. Thesis, Department of Mathematics, University of Texas at Austin, 1985."},{"key":"CR21","unstructured":"Clarke, E. M., Long, D. E., Michaylov, S., Schwab, S. A., Vidal, J.-P. and Kimura, S.: Parallel symbolic computation algorithms, Technical Report CMU-CS-90-182, School of Computer Science, Carnegie Mellon University, 1990."},{"key":"CR22","unstructured":"Conry, S. E., MacIntosh, D. J. and Meyer, R. A.: DARES: A distributed automated reasoning system, inProc. 11th Conf. of the American Association for Artificial Intelligence, 1990, pp. 78?85."},{"key":"CR23","unstructured":"Denzinger, J.: Distributed knowledge-based deduction using the team work method, Technical Report, Department of Computer Science, University of Kaiserslautern, 1991."},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Lindenstrauss, N.: An abstract concurrent machine for rewriting, in H. Kirchner and W. Wechler (eds.),Proc. 2nd Conf. on Algebraic and Logic Programming, Nancy, France, October 1990, Springer-Verlag, Lecture Notes in Computer Science 463, 1990, pp. 318?331.","DOI":"10.1007\/3-540-53162-9_48"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Goguen, J. A., Leinwand, S., Meseguer, J. and Winkler, T.: The rewrite rule machine, 1988, Technical Monograph PRG-76, Oxford University Computing Laboratory, 1989.","DOI":"10.21236\/ADA210528"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Hawley, D. J.: A Buchberger algorithm for distributed memory multi-processors, inProc. Int. Conf. of the Austrian Center for Parallel Computation, Linz, Austria, 1991, Springer-Verlag, Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-55437-8_94"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/357153.357158","volume":"4","author":"C. M. Hoffmann","year":"1982","unstructured":"Hoffmann, C. M. and O'Donnell, M. J.: Programming with equations,ACM Transactions on Programming Languages and Systems 4 (1982) 83?112.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR28","doi-asserted-by":"crossref","unstructured":"Hsiang, J. and Rusinowitch, M.: On word problems in equational theories, in Th. Ottman (ed.),Proc. 14th Int. Conf. on Automata, Languages and Programming, Karlsruhe, Germany, 1987, Springer-Verlag, Lecture Notes in Computer Science 267, 1987, pp. 54?71.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"CR29","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF00263447","volume":"8","author":"A. Jindal","year":"1992","unstructured":"Jindal, A., Overbeek, R. and Kabat, W.: Exploitation of parallel processing for implementing high-performance deduction systems,Journal of Automated Reasoning 8 (1992), 23?38.","journal-title":"Journal of Automated Reasoning"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Kapur, D. and Zhang, H.: RRL: A rewrite rule laboratory, in E. Lusk and R. Overbeek (eds.),Proc. 9th Int. Conf. on Automated Deduction, Argonne, Illinois, May 1988, Springer-Verlag, Lecture Notes in Computer Science 310, 1988, pp. 768?770.","DOI":"10.1007\/BFb0012889"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Kaser, O., Pawagi, S., Ramakrishnan, C. R., Ramakrishnan, I. V. and Sekar, R. C.: Fast parallel implementations of lazy languages ? the EQUALS experience, inProc. of the ACM Conf. on LISP and Functional Programming, 1992, pp. 335?344.","DOI":"10.1145\/141478.141570"},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Kirchner, C. and Viry, P.: Implementing parallel rewriting, in B. Fronh\u00f6fer and G. Wrightson (eds.),Parallelization in Inference Systems, Springer-Verlag, Lecture Notes in Artificial Intelligence 590, 1992, pp. 123?138.","DOI":"10.1007\/3-540-55425-4_5"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Knuth, D. and Bendix, P.: Simple word problems in universal algebra, in J. Leech (ed.),Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp. 263?297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R. E.: Depth-first iterative deepending: An optimal admissible tree search,Artificial Intelligence 27 (1985), 97?109.","journal-title":"Artificial Intelligence"},{"issue":"4","key":"CR35","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R.: A proof procedure using connection graphs,Journal of the ACM 22(4) (1975), 572?595.","journal-title":"Journal of the ACM"},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"Loganantharaj, R.: Theoretical and Implementational Aspects of Parallel Link Resolution in Connection Graphs, Ph.D. Thesis, Department of Computer Science, Colorado State University, 1985.","DOI":"10.1007\/3-540-16780-3_101"},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"Loganantharaj, R. and M\u00fcller, R. A.: Parallel theorem proving with connection graphs, in Siekmann J. (ed.),Proc. 8th Conf. on Automated Deduction, Oxford, England, 1986, Springer-Verlag, Lecture Notes in Computer Science 230, 1986, pp. 337?352.","DOI":"10.1007\/3-540-16780-3_101"},{"key":"CR38","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D. W.: A simplified format for the model elimination procedure,Journal of the ACM 16 (1969), 349?363.","journal-title":"Journal of the ACM"},{"key":"CR39","doi-asserted-by":"crossref","unstructured":"Lusk, E. L. and McCune, W. W.: Experiments with ROO: A parallel automated automated deduction system, in B. Fronh\u00f6fer and G. Wrightson (eds.),Parallelization in Inference Systems, Springer-Verlag, Lecture Notes in Artificial Intelligence 590, 1992, pp. 139?162.","DOI":"10.1007\/3-540-55425-4_6"},{"key":"CR40","series-title":"Technical Report","volume-title":"OTTER 2.0 Users Guide","author":"W. W. McCune","year":"1990","unstructured":"McCune, W. W.: OTTER 2.0 Users Guide, Technical Report ANL-90\/9, Argonne National Laboratory, Argonne, Illinois, 1990."},{"key":"CR41","series-title":"Technical Memorandum","volume-title":"What's New in OTTER 2.2","author":"W. W. McCune","year":"1991","unstructured":"McCune, W. W.: What's New in OTTER 2.2, Technical Memorandum ANL\/MCS-TM-153, Argonne National Laboratory, Argonne, Illinois, 1991."},{"key":"CR42","doi-asserted-by":"crossref","unstructured":"Schumann, J. and Letz, R.: PARTHEO: A high-performance parallel theorem prover, in M. E. Stickel (ed.),Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Germany, 1990, Springer-Verlag, Lecture Notes in Artificial Intelligence 449, 1990, pp. 28?39.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"CR43","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Parallel theorem provers ? An overview, in B. Fronh\u00f6fer and G. Wrightson (eds.),Parallelization in Inference Systems, Springer-Verlag, Lecture Notes in Artificial Intelligence 590, 1992, pp. 26?50.","DOI":"10.1007\/3-540-55425-4_2"},{"key":"CR44","unstructured":"Siegel, K.: Gr\u00f6bner Bases Computation in STRAND: A Case Study for Concurrent Symbolic Computation in Logic Programming Languages, Master Thesis and Technical Report N. 90-54.0, RISC-LINZ, 1990."},{"key":"CR45","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M. E. Stickel","year":"1984","unstructured":"Stickel, M. E.: A Prolog technology theorem prover,New Generation Computing 2 (1984), 371?383.","journal-title":"New Generation Computing"},{"key":"CR46","unstructured":"Stickel, M. E. and Tyson, W. M.: An analysis of consecutively bounded depth-first search with applications in automated deduction,Proc. 9th Int. Joint Conf. on Artificial Intelligence, Los Angeles, California, 1985, pp. 1073?1975."},{"key":"CR47","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E.: A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler,Journal of Automated Reasoning 4 (1988), 353?380.","journal-title":"Journal of Automated Reasoning"},{"key":"CR48","unstructured":"Suttner, C. B. and Schumann, J.: Parallel Automated Theorem Proving, unpublished manuscript, 1993."},{"key":"CR49","doi-asserted-by":"crossref","unstructured":"Vidal, J.-P.: The computation of Gr\u00f6bner bases on a shared memory multiprocessor, in A. Miola (ed.),Proc. Int. Symp. on the Design and Implementation of Symbolic Computation Systems, Capri, Italy, 1990, Springer-Verlag, Lecture Notes in Computer Science 429, 1990, 81?90, Full version available as Technical Report CMU-CS-90-163, School of Computer Science, Carnegie Mellon University, 1990.","DOI":"10.1007\/3-540-52531-9_127"},{"key":"CR50","volume-title":"An abstract Prolog instruction set, Technical Note 309","author":"D. H. D. Warren","year":"1983","unstructured":"Warren, D. H. D.: An abstract Prolog instruction set, Technical Note 309, Artificial Intelligence Center, SRI International, Menlo Park, California, 1983."},{"key":"CR51","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Carson, D. and Robinson, G.: Efficiency and completeness of the set of support strategy in theorem proving,Journal of the ACM 12 (1965), 536?541.","journal-title":"Journal of the ACM"},{"key":"CR52","first-page":"125","volume":"2","author":"W. T. Wu","year":"1982","unstructured":"Wu, W. T.: Mechanical theorem proving in elementary geometry and differential geometry, inProc. of the 1980 Beijing Symp. on Differential Geometry and Differential Equations 2 (1982), 125?138.","journal-title":"Proc. of the 1980 Beijing Symp. on Differential Geometry and Differential Equations"},{"key":"CR53","unstructured":"Yelick, K. A.: Using Abstraction in Explicitly Parallel Programs, Ph.D. Thesis, Laboratory for Computer Science, Massachussets Institute of Technology, available as Technical Report MIT\/LCS\/TR-507, 1991."},{"key":"CR54","doi-asserted-by":"crossref","unstructured":"Yelick, K. A. and Garland, S. J.: A parallel completion procedure for term rewriting systems, in D. Kapur (ed.),Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, New York, June 1992, Springer-Verlag, Lecture Notes in Artificial Intelligence 607, 1992, pp. 109?123.","DOI":"10.1007\/3-540-55602-8_159"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881910.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881910\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881910","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,21]],"date-time":"2024-12-21T17:47:55Z","timestamp":1734803275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881910"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881910"],"URL":"https:\/\/doi.org\/10.1007\/bf00881910","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}