{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:45Z","timestamp":1749182805795,"version":"3.41.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"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":[[1998,6]]},"DOI":"10.1023\/a:1005843328643","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"255-282","source":"Crossref","is-referenced-by-count":5,"title":["The Heine\u2013Borel Challenge Problem. In Honor of Woody Bledsoe"],"prefix":"10.1007","volume":"20","author":[{"given":"Erica","family":"Melis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"145941_CR1","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0004-3702(72)90041-0","volume":"3","author":"W. W. Bledsoe","year":"1972","unstructured":"Bledsoe, W. W., Boyer, Robert S. and Henneman, W. H.: Computer proofs of limit theorems, Artificial Intelligence\n3(1) (1972), 27\u201360.","journal-title":"Artificial Intelligence"},{"key":"145941_CR2","first-page":"1","volume":"9","author":"W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.: Non-resolution theorem proving, ficial Intelligence\n9 (1977), 1\u201335.","journal-title":"ficial Intelligence"},{"key":"145941_CR3","volume-title":"The use of analogy in automatic proof discovery","author":"W. W. Bledsoe","year":"1986","unstructured":"Bledsoe, W. W.: The use of analogy in automatic proof discovery, Tech. Rep. AI-158-86, Microelectronics and Computer Technology Corporation, Austin, TX, 1986."},{"key":"145941_CR4","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. Bledsoe","year":"1990","unstructured":"Bledsoe, W.: Challenge problems in elementary analysis, Journal of Automated Reasoning\n6 (1990), 341\u2013359.","journal-title":"Journal of Automated Reasoning"},{"key":"145941_CR5","series-title":"Technical Report Memo","volume-title":"Heine\u2013Borel Theorem Analogy Example","author":"W. W. Bledsoe","year":"1994","unstructured":"Bledsoe, W. W.: Heine\u2013Borel Theorem Analogy Example, Technical Report Memo ATP 124, University of Texas Computer Science Dept., Austin, TX, 1994."},{"key":"145941_CR6","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0303-2647(94)01453-E","volume":"34","author":"W. W. Bledsoe","year":"1995","unstructured":"Bledsoe, W. W.: A precondition prover for analogy, BioSystems\n34 (1995), 225\u2013247.","journal-title":"BioSystems"},{"key":"145941_CR7","series-title":"Technical Report Memo","volume-title":"Abduction Rules","author":"W. W. Bledsoe","year":"1995","unstructured":"Bledsoe, W. W.: Abduction Rules, Technical Report Memo ATP 126, University of Texas Computer Science Dept., Austin, TX, August 1995."},{"key":"145941_CR8","first-page":"83","volume":"11","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S. and Moore, J. S.: integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic, Machine Intelligence\n11 (1988), 83\u2013124.","journal-title":"Machine Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs, in E. Lusk and R. Overbeek (eds), Proc. 9th International Conference on Automated Deduction (CADE-9) Vol. 310, Lecture Notes in Computer Science, Springer, Argonne, 1988, pp. 111\u2013120.","key":"145941_CR9","DOI":"10.1007\/BFb0012826"},{"key":"145941_CR10","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J. and Smaill, A.: Experiments with proof plans for induction, J. Automated Reasoning\n7 (1991), 303\u2013324.","journal-title":"J. Automated Reasoning"},{"key":"145941_CR11","first-page":"371","volume-title":"Machine Learning: An Artificial Intelligence Approach","author":"J. G. Carbonell","year":"1986","unstructured":"Carbonell, J. G.: Derivational analogy: A theory of reconstructive problem solving and expertise acquisition, in R. S. Michalsky, J. G. Carbonell, and T. M. Mitchell (eds), Machine Learning: An Artificial Intelligence Approach, Morgan Kaufmann Publ., Los Altos, 1986, pp. 371\u2013392."},{"key":"145941_CR12","volume-title":"Proc. 14th International Conference on Automated Deduction (CADE)","author":"C. Benzmueller","year":"1997","unstructured":"Benzmueller, C., Cheikhrouhou, L. O., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J. and Sorge, V.: OMEGA: Towards a mathematical assistant, in Proc. 14th International Conference on Automated Deduction (CADE), Springer, Townsville, 1997."},{"key":"145941_CR13","volume-title":"Outils pour la Preuve par Analogie","author":"R. Curien","year":"1995","unstructured":"Curien, R.: Outils pour la Preuve par Analogie, PhD thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy, 1995."},{"key":"145941_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-65275-2","volume-title":"Halbgruppen und Automaten, Vol. 99 ofHeidelberger Taschenb\u00fccher","author":"P. Deussen","year":"1971","unstructured":"Deussen, P.: Halbgruppen und Automaten, Vol. 99 ofHeidelberger Taschenb\u00fccher, Springer, Berlin, 1971."},{"key":"145941_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R. and Wadsworth, C. P.: Edinburgh LCF: A Mechanized Logic of Computation, Vol. 78 of Lecture Notes in Computer Science. Springer, Berlin, 1979."},{"key":"145941_CR16","volume-title":"The Psychology of Invention in the Mathematical Field","author":"J. Hadamard","year":"1945","unstructured":"Hadamard, J.: The Psychology of Invention in the Mathematical Field, Princeton Univ. Press, Princeton, 1945."},{"key":"145941_CR17","volume-title":"Proceedings of Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz KI-94","author":"X. Huang","year":"1994","unstructured":"Huang, X., Kerber, M., Kohlhase, M. and Richts, J.: Methods \u2013 the basic units for planning and verifying proofs, in Proceedings of Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz KI-94, Springer, Saarbr\u00fccken, 1994."},{"key":"145941_CR18","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\n2 (1971), 147\u2013178.","journal-title":"Artificial Intelligence"},{"unstructured":"Kolbe, Th. and Walther, Ch.: Reusing proofs, in Proceedings of 11th European Conference on Artificial Intelligence (ECAI-94), Amsterdam, 1994.","key":"145941_CR19"},{"doi-asserted-by":"crossref","unstructured":"Kolbe, Th. and Walther, Ch.: Patching proofs for reuse, in N. Lavrac and S. Wrobel (eds), Proceedings of the 8th European Conference on Machine Learning 1995, Kreta, 1995.","key":"145941_CR20","DOI":"10.1007\/3-540-59286-5_73"},{"key":"145941_CR21","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, Mathematics and Computer Science Division, Argonne, Illinois, 1990."},{"key":"145941_CR22","series-title":"SEKI-Report","volume-title":"Analogies between Proofs \u2013 a Case Study","author":"E. Melis","year":"1993","unstructured":"Melis, E.: Analogies between Proofs \u2013 a Case Study, SEKI-Report SR-93-12, University of Saarbr\u00fccken, Saarbr\u00fccken, 1993. Available from http:\/\/jswww.ags.uni-sb.de\/pub\/seki\/index.html."},{"key":"145941_CR23","series-title":"SEKI-Report","volume-title":"Change of Representation in Theorem Proving by Analogy","author":"E. Melis","year":"1993","unstructured":"Melis, E.: Change of Representation in Theorem Proving by Analogy, SEKI-Report SR-93-07, University of Saarbr\u00fccken, Saarbr\u00fccken, 1993. Available from http:\/\/jswww.ags.uni-sb.de\/pub\/seki\/index.html."},{"key":"145941_CR24","series-title":"Technical Report DAI Research Paper","volume-title":"Analogy in CLAM","author":"E. Melis","year":"1995","unstructured":"Melis, E.: Analogy in CLAM, Technical Report DAI Research Paper No 766, University of Edinburgh, AI Dept., Dept. of Artificial Intelligence, Edinburgh, 1995. Available from http:\/\/jswww.cs.uni-sb.de\/\"melis\/."},{"unstructured":"Melis, E.: A model of analogy-driven proof-plan construction, in Proceedings of the 14th International Joint Conference on Artificial Intelligence, Montreal, 1995, pp. 182\u2013189.","key":"145941_CR25"},{"key":"145941_CR26","volume-title":"Analogy as a Means of Discovery in Problem Solving and Learning","author":"J. C. Munyer","year":"1981","unstructured":"Munyer, J. C.: Analogy as a Means of Discovery in Problem Solving and Learning, PhD thesis, University of California, Santa Cruz, 1981."},{"unstructured":"Melis, E. and Veloso, M.: Analogy makes proofs feasible, in D. Aha (ed.), AAAI-Workshop on Case-Based Reasoning, Seattle, 1994, pp. 13\u201317.","key":"145941_CR27"},{"key":"145941_CR28","volume-title":"Analogy for Automated Reasoning","author":"S. Owen","year":"1990","unstructured":"Owen, S.: Analogy for Automated Reasoning, Academic Press, New York, 1990."},{"doi-asserted-by":"crossref","unstructured":"Polya, G.: How to Solve It, Princeton University Press, 1945.","key":"145941_CR29","DOI":"10.1515\/9781400828678"},{"doi-asserted-by":"crossref","unstructured":"Polya, G.: Mathematics and Plausible Reasoning, Princeton University Press, 1954.","key":"145941_CR30","DOI":"10.1515\/9780691218304"},{"unstructured":"Sehn, A. C.: DECLAME \u2013 eine deklarative Sprache zur Repr\u00e4sentation von Methoden, Master's thesis, Universit\u00e4t des Saarlandes, 1995, published as SEKI Working Paper SWP-95-02.","key":"145941_CR31"},{"doi-asserted-by":"crossref","unstructured":"van der Waerden, B. L.: Wie der Beweis der Vermutung von Baudet gefunden wurde, Abh. Math. Sem. Univ. Hamburg\n28 (1964).","key":"145941_CR32","DOI":"10.1007\/BF02993133"},{"unstructured":"Veloso, M. M.: Flexible strategy learning: Analogical replay of problem solving episodes, in Proc. of the Twelfth National Conference on Artificial Intelligence 1994, Seattle, WA, 1994.","key":"145941_CR33"},{"key":"145941_CR34","volume-title":"The Use of Analogy in the PC System","author":"R. Wang","year":"1991","unstructured":"Wang, R.: The Use of Analogy in the PC System, Computer Science Department Memo, Univerity of Texas at Austin, May 1991."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005843328643.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005843328643\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005843328643.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:25:42Z","timestamp":1749122742000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005843328643"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["145941"],"URL":"https:\/\/doi.org\/10.1023\/a:1005843328643","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}