{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T09:07:00Z","timestamp":1648717620920},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2004,9,1]],"date-time":"2004-09-01T00:00:00Z","timestamp":1093996800000},"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":[[2004,9]]},"DOI":"10.1007\/s10817-004-3243-2","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T18:23:02Z","timestamp":1108750982000},"page":"171-218","source":"Crossref","is-referenced-by-count":2,"title":["Octopus: Combining Learning and Parallel Search"],"prefix":"10.1007","volume":"33","author":[{"given":"Monty","family":"Newborn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyan","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,2,14]]},"reference":[{"key":"CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-0089-2","volume-title":"Automated Theorem Proving: Theory and Practice","author":"M. Newborn","year":"2001","unstructured":"Newborn, M.: Automated Theorem Proving: Theory and Practice, Springer-Verlag, New York, 2001."},{"issue":"2","key":"CR2","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G. and Suttner, C. B.: The TPTP problem library, J. Automated Reasoning 21(2) (1998), 177?203.","journal-title":"J. Automated Reasoning"},{"key":"CR3","unstructured":"http:\/\/www.cs.miami.edu\/~tptp\/"},{"key":"CR4","unstructured":"http:\/\/www.cs.miami.edu\/~tptp\/CASC\/"},{"key":"CR5","unstructured":"Newborn, M.: Proofs of twenty-four 1.0-rated theorems in the TPTP problem library, TR SOCS-03.6, School of Computer Science, McGill University, Montreal, 2003."},{"key":"CR6","unstructured":"Newborn, M. and Wang, Z.: Proofs of nineteen more 1.0 rated theorems in the TPTP problem library, TR SOCS-04.1, School of Computer Science, McGill University, Montreal, 2004."},{"issue":"1","key":"CR7","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D. A. Plaisted","year":"1981","unstructured":"Plaisted, D. A.: Theorem proving with abstraction, Artificial Intelligence 16(1) (1981), 47?108.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"CR8","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/0004-3702(71)90008-7","volume":"2","author":"R. E. Kling","year":"1971","unstructured":"Kling, R. E.: A paradigm for reasoning by analogy, Artificial Intelligence 2(2) (1971), 147?178.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"CR9","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/0004-3702(88)90032-X","volume":"35","author":"R. Greiner","year":"1988","unstructured":"Greiner, R.: Learning and understanding by analogies, Artificial Intelligence 35(1) (1988), 81?125.","journal-title":"Artificial Intelligence"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Brock, B., Cooper, S. and Pierce, W.: Analogical reasoning and proof discovery, in E. Lusk and R. A. Overbeek (eds.), Proc. 9th Conf. on Automated Deduction, Argonne, IL, LNCS 310, Springer-Verlag, 1988, pp. 454?468.","DOI":"10.1007\/BFb0012849"},{"key":"CR11","unstructured":"Carbonell, J. G. and Veloso, M.: Integrating derivational analogy into a general problem solving architecture, in J. Kolodner (ed.), Proc. 1988 DARPA Workshop on Case-Based Reasoning, Clearwater Beach, 1988."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Kolbe, T. and Brauburger, J.: Plagiator ? a learning prover, in W. McCune (ed.), Proc. 14th Int. Conf. on Automated Deduction, LNCS 1249, Springer-Verlag, 1997, pp. 256?259.","DOI":"10.1007\/3-540-63104-6_24"},{"key":"CR13","unstructured":"Kolbe, T. and Walther, C.: Reusing proofs, in A. G. Cohn (ed.), Proc. 11th European Conf. on Artificial Intelligence, Amsterdam, Wiley, 1994, pp. 80?84."},{"key":"CR14","unstructured":"Melis, E.: A model of analogy-driven proof-plan construction, in C. S. Mellish (ed.), Proc. 14th Int. Joint Conf. on Artificial Intelligence, Morgan Kaufmann, 1995, pp. 182?189."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Draeger, J.: Acquisition of useful lemma knowledge in automated reasoning, in F. Giunchiglia (ed.), Proc. 8th Int. Conf. on Artificial Intelligence: Methodology, Systems, and Applications, LNCS 1480, Springer-Verlag, 1998, pp. 230?239.","DOI":"10.1007\/BFb0057448"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Fuchs, M.: Experiments in the heuristic use of past proof experience, in M. A. McRobbie and J. K. Slaney (eds.), Proc. 13th Conf. on Automated Deduction, LNAI 1104, Springer-Verlag, 1996, pp. 523?537.","DOI":"10.1007\/3-540-61511-3_111"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Denzinger, J. and Schulz, S.: Learning domain knowledge to improve theorem proving, in M. A. McRobbie and J. K. Slaney (eds.), Proc. 13th Conf. on Automated Deduction, LNAI 1104, Springer-Verlag, 1996, pp. 62?76.","DOI":"10.1007\/3-540-61511-3_69"},{"key":"CR18","unstructured":"Denzinger, J., Fuchs, M., Goller, C. and Schulz, S.: Learning from previous proof experience: A survey, Report AR-99-4, Fakult\u00e4t f\u00fcr Informatik der Technischen Universit\u00e4t M\u00fcnchen, 1999."},{"issue":"1?4","key":"CR19","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1023\/A:1018932114059","volume":"29","author":"M. P. Bonacina","year":"2000","unstructured":"Bonacina, M. P.: A taxonomy of parallel strategies for deduction, Ann. Math. Artificial Intelligence 29(1?4) (2000), 223?257.","journal-title":"Ann. Math. Artificial Intelligence"},{"issue":"1","key":"CR20","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, J. Automated Reasoning 8(1) (1992), 23?38.","journal-title":"J. Automated Reasoning"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"Lusk, E. L. and McCune, W. W.: Experiments with ROO: A parallel automated deduction system, in B. Fronhofer and G. Wrightson (eds.), Parallelization in Inference Systems, LNAI 590, Springer-Verlag, 1990, pp. 139?162.","DOI":"10.1007\/3-540-55425-4_6"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Lusk, E., McCune, W. and Slaney, J.: ROO ? a parallel theorem prover, ANL\/MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.","DOI":"10.2172\/5796402"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Lusk, E. L., McCune, W. W. and Slaney, J. K.: ROO: A parallel theorem prover, in D. Kapur (ed.), Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, June 15?18, LNAI 607, Springer-Verlag, 1992, pp. 731?734.","DOI":"10.1007\/3-540-55602-8_213"},{"issue":"3","key":"CR24","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 Computation 19(3) (1995), 245?267.","journal-title":"J. Symbolic Computation"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P.: Combination of distributed search and multi-search in Peers-mcd.d, in R. Gore, A. Leitsch and T. Nipkow (eds.), Proc. 1st Int. Joint Conf. on Automated Reasoning, Siena, Italy, June 18?23, LNAI 2083, Springer-Verlag, 2001, pp. 448?452.","DOI":"10.1007\/3-540-45744-5_37"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Bonacina, M. P.: The clause-diffusion theorem prover Peers-mcd (system description), in W. McCune (ed.), Proc. 14th Int. Conf. on Automated Deduction, Townsville, Australia, July 13?17, LNCS 1249, Springer-Verlag, 1997, pp. 53?56.","DOI":"10.1007\/3-540-63104-6_6"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 3.3 reference manual, Technical Memorandum No. 263, Mathematics and Computer Science Division, Argonne National Laboratory, 2003 (http:\/\/www-unix.mcs.anl.gov\/AR\/otter\/otter33.pdf).","DOI":"10.2172\/822573"},{"key":"CR28","unstructured":"McCune, W.: 33 basic test problems: A practical evaluation of some paramodulation strategies, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1997."},{"issue":"5\/6","key":"CR29","first-page":"183","volume":"15","author":"R. Letz","year":"1992","unstructured":"Letz, R., Bayerl, S., Schumann, J. and Bibil, W.: SETHEO ? a high-performance theorem prover, J. Symbolic Computation 15(5\/6) (1992), 183?212.","journal-title":"J. Symbolic Computation"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Fuchs, M. and Wolf, A.: System description ? Cooperation in model elimination: CPTHEO, in C. Kirchner and H. Kirchner (eds.), Proc. 15th Int. Conf. on Automated Deduction, LNCS 1421, Springer-Verlag, 1998, pp. 42?46.","DOI":"10.1007\/BFb0054245"},{"key":"CR31","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, LNAI 449, Springer-Verlag, 1990, pp. 40?56.","DOI":"10.1007\/3-540-52885-7_78"},{"issue":"2","key":"CR32","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, J. Automated Reasoning 8(2) (1992), 153?181.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"CR33","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF00881946","volume":"13","author":"O. Astrachan","year":"1994","unstructured":"Astrachan, O.: METEOR: Exploring model elimination theorem proving, J. Automated Reasoning 13(3) (1994), 283?296.","journal-title":"J. Automated Reasoning"},{"key":"CR34","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, 1991, pp. 31?60.","DOI":"10.1007\/978-94-011-3488-0_2"},{"issue":"6","key":"CR35","doi-asserted-by":"crossref","first-page":"1307","DOI":"10.1109\/21.135677","volume":"21","author":"D. J. MacIntosh","year":"1991","unstructured":"MacIntosh, D. J., Conry, S. E. and Meyer, R. A.: Distributed automated reasoning: Issues in coordination, cooperation and performance, IEEE Trans. Systems, Man, Cybernet. 21(6) (1991), 1307?1316.","journal-title":"IEEE Trans. Systems, Man, Cybernet."},{"issue":"2","key":"CR36","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J. Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M. and Schulz, S.: DISCOUNT ? a distributed and learning equational prover, J. Automated Reasoning 18(2) (1997), 189?198.","journal-title":"J. Automated Reasoning"},{"key":"CR37","unstructured":"Denzinger, J. and Fuchs, D.: Cooperation of heterogeneous provers, in T. Dean (ed.), Proc. of the 16th Int. Joint Conf. on Artificial Intelligence, Stockholm, Sweden, July 31?August 6, Morgan Kaufmann, 1999, pp. 10?15."},{"issue":"2","key":"CR38","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: Spass: Version 0.49, J. Automated Reasoning 18(2) (1997), 247?252.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"CR39","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 18(2) (1997), 253?258.","journal-title":"J. Automated Reasoning"},{"issue":"4","key":"CR40","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1023\/A:1006127022180","volume":"22","author":"C. B. Suttner","year":"1999","unstructured":"Suttner, C. B.: SPS-Parallelism+SETHEO=SPTHEO, J. Automated Reasoning 22(4) (1999), 397?431.","journal-title":"J. Automated Reasoning"},{"key":"CR41","unstructured":"Wolf, A.: p-SETHEO: Strategy parallelism in automated theorem proving, in H. de Swert (ed.), Proc. Int. Conf. TABLEAUX?98: Analytic Tableaux and Related Methods, LNAI 397, Springer-Verlag, 1998, pp. 320?324."},{"key":"CR42","doi-asserted-by":"crossref","unstructured":"Schumann, J.: SiCoTHEO ? Simple competitive parallel theorem provers based on SETHEO, in J. Geller, H. Kitano and C. B. Suttner (eds.), Parallel Processing for Artificial Intelligence 3, Elsevier, 1997, pp. 231?245.","DOI":"10.1016\/S0923-0459(97)80012-2"},{"key":"CR43","unstructured":"Sutcliffe, G. and Seyfang, D.: Smart selective competition parallelism ATP, in A. Kumar and I. Russell (eds.), Proc. 12th Florida Artificial Intelligence Research Symposium, Orlando, FL, May 3?5, American Association for Artificial Intelligence Press, 1999, pp. 341?345."},{"key":"CR44","unstructured":"De Nivelle, H.: Bliksem 1.00, in C. Kirchner and H. Kirchner (eds.), Proc. 15th Int. Conf. on Automated Deduction, Lindau, Germany, July 5?10, LNCS 1421, Springer-Verlag, 1998, p. 9."},{"issue":"2","key":"CR45","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf, J. Automated Reasoning 18(2) (1997), 247?252.","journal-title":"J. Automated Reasoning"},{"key":"CR46","unstructured":"McCune, W.: Otter 3.3 Reference Manual, Technical Memorandum No. 249, Mathematics and Computer Science Division, Argonne National Laboratory, 2001 (http:\/\/www-unix.mcs.anl.gov\/AR\/mace2\/mace2.pdf)."},{"key":"CR47","unstructured":"http:\/\/www.cs.miami.edu\/~tptp\/CASC\/16\/"},{"key":"CR48","unstructured":"Newborn, M.: The Great Theorem Prover, Newborn Software, 1989."},{"key":"CR49","unstructured":"http:\/\/www.cs.miami.edu\/~tptp\/CASC\/19\/"},{"key":"CR50","doi-asserted-by":"crossref","unstructured":"Geist, A., Beguelin, A., Dongarra, J., Jiang, W., Manchek, R. and Sunderam, V.: PVM: Parallel Virtual Machine, MIT Press, 1994.","DOI":"10.7551\/mitpress\/5712.001.0001"},{"key":"CR51","unstructured":"Draeger, J.: Anwendung des Theorembeweisers SETHEO auf angeordnete K\u00f6rper, FKI-186-93, Technische Universit\u00e4t M\u00fcnchen, Munich, 1993."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-3243-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-3243-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-3243-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T21:24:29Z","timestamp":1586121869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-3243-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,9]]}},"alternative-id":["3243"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-3243-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,9]]}}}