{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:51Z","timestamp":1749182811629,"version":"3.41.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2001,1]]},"DOI":"10.1023\/a:1006469202251","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T02:03:28Z","timestamp":1040522608000},"page":"67-106","source":"Crossref","is-referenced-by-count":1,"title":["Parallelization of a Hyper-Linking\u2013Based Theorem Prover"],"prefix":"10.1007","volume":"26","author":[{"given":"Chih-Hung","family":"Wu","sequence":"first","affiliation":[]},{"given":"Shie-Jue","family":"Lee","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"270916_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1006\/jsco.1996.0028","volume":"21","author":"M. P. Bonacina","year":"1996","unstructured":"Bonacina, M. P.: On the reconstruction of proofs in distributed theorem proving: A modified Clause-Diffusion method, J. Symbolic Comput.\n21 (1996), 507-522.","journal-title":"J. Symbolic Comput."},{"key":"270916_CR2","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P.: Experiments with subdivision of search in diftributed theorem proving, in Proceedings of the Second International Symposium on Parallel Symbolic Computation, 1997, pp. 88-100.","DOI":"10.1145\/266670.266696"},{"key":"270916_CR3","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1006\/jsco.1995.1014","volume":"19","author":"M. P. Bonacina","year":"1995","unstructured":"Bonacina, M. P. and Hsiang, J.: Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover, J. Symbolic Comput.\n19 (1995), 245-267.","journal-title":"J. Symbolic Comput."},{"key":"270916_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881910","volume":"13","author":"M. P. Bonacina","year":"1994","unstructured":"Bonacina, M. P. and Hsiang, J.: Parallelization of deduction strategies: An analytical study, J. Automated Reasoning\n13 (1994), 1-33.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR5","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P. and McCune, W.: Distributed theorem proving by Peers, in Proceedings of the 12th International Conference on Automated Deduction, 1994, pp. 841-845.","DOI":"10.1007\/3-540-58156-1_72"},{"issue":"2","key":"270916_CR6","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 Michaylon, S.: PARTHENON: A parallel theorem prover for non-Horn clauses, J. Automated Reasoning\n8(2) (1992), 153-182.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR7","volume-title":"Programming Expert Systems in OPS5: An Introduction to Rule-Based Programming","author":"L. Brownston","year":"1985","unstructured":"Brownston, L., Farrel, R., Kant, E. and Martin, N.: Programming Expert Systems in OPS5: An Introduction to Rule-Based Programming, Addison-Wesley, Reading, MA, 1985."},{"key":"270916_CR8","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1142\/S0129626496000455","volume":"6","author":"D. Cachera","year":"1996","unstructured":"Cachera, D. and Utard, G.: Proving data-parallel programs: A unifying approach, Parallel Process. Lett.\n6 (1996), 491-506.","journal-title":"Parallel Process. Lett."},{"key":"270916_CR9","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, R. C. T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"270916_CR10","unstructured":"Conry, S. E., MacIntosh, D. J. and Meyer, R. A.: DARES: A distributed automated resolution system, in Proceedings of the 11th National Conference on Artificial Intelligence, 1990, pp. 78-85."},{"issue":"3","key":"270916_CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM\n7(3) (1960), 201-215.","journal-title":"J. ACM"},{"key":"270916_CR12","volume-title":"Operating Systems","author":"H. M. Deitel","year":"1990","unstructured":"Deitel, H. M.: Operating Systems, Addison-Wesley, Reading, MA, 1990."},{"key":"270916_CR13","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0004-3702(86)90080-9","volume":"28","author":"J. de Kleer","year":"1986","unstructured":"de Kleer, J.: An assumption-based TMS, Artif. Intell.\n28 (1986), 127-162.","journal-title":"Artif. Intell."},{"key":"270916_CR14","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1006\/jsco.1996.0029","volume":"21","author":"J. Denzinger","year":"1996","unstructured":"Denzinger, J. and Schulz, S.: Recording and analyzing knowledge-based distributed deduction processes, J. Symbolic Comput.\n21 (1996), 523-541.","journal-title":"J. Symbolic Comput."},{"key":"270916_CR15","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C. L. Forgy","year":"1982","unstructured":"Forgy, C. L.: Rete: A fast algorithm for the many pattern\/many object pattern match problem, Artif. Intell.\n19 (1982), 17-37.","journal-title":"Artif. Intell."},{"key":"270916_CR16","doi-asserted-by":"crossref","unstructured":"Goubault, J.: Proving with BDDs and control of information, in Proceedings of the 12th International Conference on Automated Deduction, 1994, pp. 499-513.","DOI":"10.1007\/3-540-58156-1_36"},{"key":"270916_CR17","doi-asserted-by":"crossref","unstructured":"Graf, P.: Extended path-indexing, in Proceedings of the 12th International Conference on Automated Deduction, 1994, pp. 514-528.","DOI":"10.1007\/3-540-58156-1_37"},{"key":"270916_CR18","unstructured":"Gutpa, A.: Parallelism in production systems, Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University, 1986."},{"key":"270916_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, A., Forgy, C., Newell, A. and Wedig, R.: Parallel algorithms and architectures for rule-based systems, in Proceedings of the 13th Annual International Symposium on Computer Architecture, 1986.","DOI":"10.1145\/17356.17360"},{"key":"270916_CR20","unstructured":"Hasegawa, R. and Koshimura, M.: An AND parallelization method for MGTP and its evaluation, in Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994."},{"issue":"4","key":"270916_CR21","first-page":"376","volume":"21","author":"H. Hong","year":"1996","unstructured":"Hong, H.: Special issue on parallel symbolic computation: Foreword of the guest editor, J. Symbolic Comput.\n21(4) (1996), 376-377.","journal-title":"J. Symbolic Comput."},{"key":"270916_CR22","doi-asserted-by":"crossref","unstructured":"Konrad, K.: HOT: A concurrent automated theorem prover based on higher-order tableaux, in Lecture Notes in Comput. Sci. 1479, Springer, 1998, pp. 245-262.","DOI":"10.1007\/BFb0055140"},{"key":"270916_CR23","unstructured":"Laird, J. E. and Newell, A.: A universal weak method, Technical Report CMU-CS-83-141, Department of Computer Science, Carnegie-Mellon University, 1983."},{"issue":"1","key":"270916_CR24","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J. and Plaisted, D.: Eliminating duplication with hyper-linking strategy, J. Automated Reasoning\n9(1) (1992), 25-42.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR25","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00885766","volume":"12","author":"S.-J. Lee","year":"1994","unstructured":"Lee, S.-J. and Wu, C.-H.: Improving the efficiency of a hyper-linking based theorem prover by incremental evaluation with network structures, J. Automated Reasoning\n12 (1994), 359-388.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR26","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/3-540-55425-4_6","volume":"590","author":"E. L. Lusk","year":"1992","unstructured":"Lusk, E. L. and McCune, W. W.: Experiments with ROO: A parallel automated deduction system, Parallelization in Inference Systems\n590 (1992), 139-162.","journal-title":"Parallelization in Inference Systems"},{"key":"270916_CR27","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. W. McCune","year":"1992","unstructured":"McCune, W. W.: Experiments with discrimination-tree indexing and path indexing for term retrieval, J. Automated Reasoning\n9 (1992), 147-167.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR28","volume-title":"OTTER 3.0 Users' Guide","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: OTTER 3.0 Users' Guide, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, January 1994."},{"key":"270916_CR29","doi-asserted-by":"crossref","unstructured":"Moten, R.: Exploiting parallelism in interactive theorem provers, in Lecture Notes in Comput. Sci. 1479, Springer, 1998, pp. 315-330.","DOI":"10.1007\/BFb0055144"},{"key":"270916_CR30","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers, J. Automated Reasoning\n2 (1986), 191-216.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR31","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"Plaisted, D.: Non-Horn clause logic programming without contrapositives, J. Automated Reasoning\n4 (1988), 287-325.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR32","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Delta-a bottom-up preprocessor for top-down theorem provers (system abstract), in Proceedings of the 12th International Conference on Automated Deduction, 1994, pp. 774-777.","DOI":"10.1007\/3-540-58156-1_58"},{"key":"270916_CR33","unstructured":"Singhal, A. and Yale, P.: Unification parallelism: How much can we exploit?, in Proceedings of the North American Conference on Logic Programming, 1989, pp. 1135-1147."},{"key":"270916_CR34","doi-asserted-by":"crossref","unstructured":"Slaney, J. K. and Lusk, E. L.: Parallelizing the closure computation in automated deduction, in Proceedings of the 10th International Conference on Automated Deduction, 1990, pp. 28-39.","DOI":"10.1007\/3-540-52885-7_77"},{"key":"270916_CR35","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, J. Automated Reasoning\n4 (1988), 353-380.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR36","unstructured":"Stolfo, S. J. and Shaw, D. E.: DADO: A tree-structured machine architecture for production systems, in Proceedings of the National Conference on Artificial Intelligence, August 1982, pp. 369-388."},{"key":"270916_CR37","unstructured":"Stolfo, S. J. and Shaw, D. E.: Architecture and application of DADO: A large-scale parallel computer for artificial intelligence, in Proceedings of the International Joint Conference on Artificial Intelligence, 1983."},{"key":"270916_CR38","doi-asserted-by":"crossref","unstructured":"Sturgill, D. B. and Segre, A.M.: A novel asynchronous parallelism scheme for first-order logic, in Proceedings of the 12th International Conference on Automated Deduction, 1994, pp. 484-498.","DOI":"10.1007\/3-540-58156-1_35"},{"key":"270916_CR39","doi-asserted-by":"crossref","unstructured":"Suttner, C. B.: SPTHEO-a PVM-based parallel theorem prover, in Lecture Notes in Comput. Sci. 1156, Springer, 1996, pp. 116-125.","DOI":"10.1007\/3540617795_15"},{"key":"270916_CR40","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1023\/A:1005868304990","volume":"18","author":"C. B. Suttner","year":"1997","unstructured":"Suttner, C. B.: SPTHEO: A parallel theorem prover, J. Automated Reasoning\n18 (1997), 253-258.","journal-title":"J. Automated Reasoning"},{"key":"270916_CR41","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/B978-0-444-81704-4.50015-6","volume":"1","author":"C. B. Suttner","year":"1994","unstructured":"Suttner, C. B. and Schumann, J.: Parallel automated theorem proving, Parallel Process. Artif. Intell.\n1 (1994), 209-257.","journal-title":"Parallel Process. Artif. Intell."},{"key":"270916_CR42","series-title":"Technical Report 99\/02","volume-title":"The TPTP problem library, v2.2.0","author":"C. B. Suttner","year":"1999","unstructured":"Suttner, C. B. and Sutcliffe, G.: The TPTP problem library, v2.2.0, Technical Report 99\/02, Department of Computer Science, James Cook University, Australia, 1999."},{"key":"270916_CR43","volume-title":"SWI Prolog 3.1 Reference Manual","author":"J. Wielemaker","year":"1998","unstructured":"Wielemaker, J.: SWI Prolog 3.1 Reference Manual, Dept. of Social Science Information (SWI), University of Amsterdam, Roeterstraat 15, 1018 WB Amsterdam, The Netherlands, 1998."},{"key":"270916_CR44","doi-asserted-by":"crossref","unstructured":"Wolf, A.: P-SETHEO: Strategy parallelism in automated theorem proving, in Lecture Notes in Comput. Sci. 1397, Springer, 1998, pp. 320-324.","DOI":"10.1007\/3-540-69778-0_32"},{"key":"270916_CR45","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M. P. and Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems, J. Symbolic Comput.\n21 (1996), 543-560.","journal-title":"J. Symbolic Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006469202251.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006469202251\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006469202251.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:33:22Z","timestamp":1749123202000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006469202251"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,1]]}},"alternative-id":["270916"],"URL":"https:\/\/doi.org\/10.1023\/a:1006469202251","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,1]]}}}