{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T10:24:09Z","timestamp":1743503049135},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_43","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"644-659","source":"Crossref","is-referenced-by-count":14,"title":["Proof Planning with Multiple Strategies"],"prefix":"10.1007","author":[{"given":"Erica","family":"Melis","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Meier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"key":"43_CR1","unstructured":"Gandalf. In CASC-14 http:\/\/www.cs.jcu.edu.au\/~tptp\/casc-14\/ , 1997."},{"key":"43_CR2","volume-title":"Introduction to Real Analysis","author":"R.G. Bartle","year":"1982","unstructured":"R.G. Bartle and D.R. Sherbert. Introduction to Real Analysis. John Wiley & Sons, New York, 1982."},{"key":"43_CR3","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, A. Meier, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge. OMEGA: Towards a mathematical assistant. In Proc. CADE-14, pages 252\u2013255. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"43_CR4","unstructured":"C. Benzm\u00fcller, M. Jamnik, M. Kerber, and V. Sorge. Agent Based Mathematical Reasoning? In 7th CALCULEMUS Workshop, pages 21\u201332, 1999."},{"issue":"1","key":"43_CR5","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(72)90041-0","volume":"3","author":"W.W. Bledsoe","year":"1972","unstructured":"W.W. Bledsoe, R.S. Boyer, and W.H. Henneman. Computer proofs of limit theorems. Artificial Intelligence, 3(1):27\u201360, 1972.","journal-title":"Artificial Intelligence"},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In Proc. of CADE-9, pages 111\u2013120, 1988.","DOI":"10.1007\/BFb0012826"},{"key":"43_CR7","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"63","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. Van Harmelen, A. Ireland, and A. Smaill. A heuristic for guiding inductive proofs. Artificial Intelligence, 63:185\u2013253, 1993.","journal-title":"Artificial Intelligence"},{"key":"43_CR8","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303\u2013324, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"43_CR9","unstructured":"J. Denzinger and M. Fuchs. Cooperation of heterogeneous provers. In Proc. of IJCAI, pages 10\u201315. Morgan Kaufmann, 1999."},{"issue":"3","key":"43_CR10","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0004-3702(85)90063-3","volume":"26","author":"Barbara Hayes-Roth","year":"1985","unstructured":"B. Hayes-Roth. A blackboard architecture for control. Artificial Intelligence, pages 251\u2013321, 1985.","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"43_CR11","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1\u20132):79\u2013111, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"43_CR12","unstructured":"W.W. McCune. Otter 2.0 users guide. Technical Report ANL-90\/9, Argonne National Laboratory, 1990."},{"key":"43_CR13","unstructured":"E. Melis. AI-techniques in proof planning. In Proc. of European Conference on Artificial Intelligence, pages 494\u2013498. Kluwer, 1998."},{"key":"43_CR14","unstructured":"E. Melis. Combining proof planning with constraint solving. In Proc. of Calculemus and Types\u201998, 1998."},{"key":"43_CR15","unstructured":"E. Melis. The\u201climit\u201d domain. In Proc. of the Fourth International Conference on Artificial Intelligence in Planning Systems (AIPS\u201998), pages 199\u2013206, 1998."},{"key":"43_CR16","unstructured":"E. Melis and A. Meier. Proof planning with multiple strategies. Seki report SR-99-06, Universit\u00e4t des Saarlandes, FB Informatik, 1999."},{"key":"43_CR17","unstructured":"E. Melis and A. Meier. Proof planning with multiple strategies II. In FLoC\u201999 workshop on Strategies in Automated Deduction, pages 61\u201372, 1999."},{"key":"43_CR18","doi-asserted-by":"crossref","unstructured":"E. Melis and J.H. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 1999.","DOI":"10.1016\/S0004-3702(99)00076-4"},{"key":"43_CR19","doi-asserted-by":"crossref","unstructured":"E. Melis and C. Ullrich. Flexibly interleaving processes. In K.-D. Althoff and R. Bergmann, editors, International Conference on Case-Based Reasoning, volume 1650 of Lecture Notes in Artificial Intelligence, pages 263\u2013275. Springer, 1999.","DOI":"10.1007\/3-540-48508-2_19"},{"key":"43_CR20","doi-asserted-by":"crossref","DOI":"10.1515\/9781400828678","volume-title":"How to Solve it","author":"G. Polya","year":"1945","unstructured":"G. Polya. How to Solve it. Princeton University Press, Princeton, 1945."},{"key":"43_CR21","volume-title":"Mathematical Problem Solving","author":"A.H. Schoenfeld","year":"1985","unstructured":"A.H. Schoenfeld. Mathematical Problem Solving. Academic Press, New York, 1985."},{"issue":"4","key":"43_CR22","first-page":"27","volume":"15","author":"D.S. Weld","year":"1994","unstructured":"D.S. Weld. An introduction to least committment planning. AI magazine, 15(4):27\u201361, 1994.","journal-title":"AI magazine"},{"key":"43_CR23","unstructured":"D.E. Wilkins and K.L. Myers. A multiagent planning architecture. In Proc. of the Fourth International Conference on AI Planning Systems (AIPS\u201998), pages 154\u2013162, 1998."},{"key":"43_CR24","doi-asserted-by":"crossref","unstructured":"A. Wolf. Strategy selection for automated theorem proving. In Proc. of AIMSA\u2019 98, pages 452\u2013465, 1998.","DOI":"10.1007\/BFb0057466"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T16:27:30Z","timestamp":1587572850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_43","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}