{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:28Z","timestamp":1725576268840},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232124"},{"type":"electronic","value":"9783540302100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30210-0_4","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:34:36Z","timestamp":1295346876000},"page":"26-37","source":"Crossref","is-referenced-by-count":1,"title":["Planning and Patching Proof"],"prefix":"10.1007","author":[{"given":"Alan","family":"Bundy","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","first-page":"116","volume-title":"Proc. 13th Intern. Joint Conference on Artificial Intelligence (IJCAI 1993)","author":"D.A. Basin","year":"1993","unstructured":"Basin, D.A., Walsh, T.: Difference unification. In: Bajcsy, R. (ed.) Proc. 13th Intern. Joint Conference on Artificial Intelligence (IJCAI 1993), vol.\u00a01, pp. 116\u2013122. Morgan Kaufmann, San Francisco (1993); Also available as Technical Report MPI-I-92-247, Max-Planck-Institut f\u00fcr Informatik"},{"issue":"1-2","key":"4_CR2","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. Journal of Automated Reasoning\u00a016(1-2), 147\u2013180 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"14th International Conference on Automated Deduction","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J., Sorge, V.: \u03a9mega: Towards a mathematical assistant. In: McCune, W. (ed.) 14th International Conference on Automated Deduction, pp. 252\u2013255. Springer, Heidelberg (1997)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0055131","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Boulton","year":"1998","unstructured":"Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 87\u2013104. Springer, Heidelberg (1998)"},{"key":"4_CR5","unstructured":"Bundy, A., Green, I.: An experimental comparison of rippling and exhaustive rewriting. Research paper 836, Dept. of Artificial Intelligence, University of Edinburgh (December 1996)"},{"key":"4_CR6","unstructured":"Bundy, A., Lombart, V.: Relational rippling: a general approach. In: Mellish, C. (ed.) Proceedings of IJCAI, pp. 175\u2013181 (1995)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111\u2013120. Springer, Heidelberg (1988); Longer version available from Edinburgh as DAI Research Paper No. 349"},{"key":"4_CR8","first-page":"178","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"A.. Bundy","year":"1991","unstructured":"Bundy, A.: A science of reasoning. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178\u2013198. MIT Press, Cambridge (1991); Also available from Edinburgh as DAI Research Paper 445"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning","author":"A. Bundy","year":"2001","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, Elsevier, Amsterdam (2001)"},{"key":"4_CR10","first-page":"160","volume-title":"A Critique of Proof Planning","author":"A. Bundy","year":"2002","unstructured":"Bundy, A.: A Critique of Proof Planning, pp. 160\u2013177. Springer, Heidelberg (2002)"},{"key":"4_CR11","first-page":"359","volume-title":"Proceedings of the Eleventh International Joint Conference on Artificial Intelligence","author":"A. Bundy","year":"1989","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A., Stevens, A.: A rational reconstruction and extension of recursion analysis. In: Sridharan, N.S. (ed.) Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pp. 359\u2013365. Morgan Kaufmann, San Francisco (1989); Also available from Edinburgh as DAI Research Paper 419"},{"key":"4_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990); Also available from Edinburgh as DAI Research Paper 507"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062, 185\u2013253 (1993); Also available from Edinburgh as DAI Research Paper No. 567","journal-title":"Artificial Intelligence"},{"key":"4_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-level Guidance for Mathematical Reasoning","author":"A. Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1018940332714","volume":"29","author":"L. Dennis","year":"2000","unstructured":"Dennis, L., Bundy, A., Green, I.: Making a productive use of failure to generate witness for coinduction from divergent proof attempts. Annals of Mathematics and Artificial Intelligence\u00a029, 99\u2013138 (2000); Also available as paper No. RR0004 in the Informatics Report Series","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"#cr-split#-4_CR16.1","unstructured":"Desimone, R.V.: Explanation-Based Learning of Proof Plans. In: Kodratoff, Y., Hutchinson, A. (eds.) Machine and Human Learning, Kogan Page (1989);"},{"key":"#cr-split#-4_CR16.2","unstructured":"Also available as DAI Research Paper 304. Previous version in proceedings of EWSL 1986 (1986)"},{"key":"4_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L. Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.D.: IsaPlanner: A prototype proof planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"4_CR18","unstructured":"Duncan, H., Bundy, A., Levine, J., Storkey, A., Pollet, M. (2004). The use of data-mining for the automatic formation of tactics. In: Workshop on Computer-Supported Mathematical Theory Development. IJCAR 2004 (2004)"},{"issue":"1-2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0004-3702(97)00082-9","volume":"100","author":"I. Frank","year":"1998","unstructured":"Frank, I., Basin, D.: Search in games with incomplete information: A case study using bridge card play. Artificial Intelligence\u00a0100(1-2), 87\u2013123 (1998)","journal-title":"Artificial Intelligence"},{"key":"#cr-split#-4_CR20.1","unstructured":"Frank, I., Basin, D., Bundy, A.: An adaptation of proofplanning to declarer play in bridge. In: Proceedings of ECAI, pp. 72???76, Vienna, Austria (1992);"},{"key":"#cr-split#-4_CR20.2","unstructured":"Longer Version available from Edinburgh as DAI Research Paper No. 575"},{"key":"4_CR21","unstructured":"Gow, J.: The Dynamic Creation of Induction Rules Using Proof Planning. Unpublished Ph.D. thesis, Division of Informatics, University of Edinburgh (2004)"},{"key":"4_CR22","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/3-540-63104-6_30","volume-title":"14th International Conference on Automated Deduction","author":"D. Hutter","year":"1997","unstructured":"Hutter, D., Kohlhase, M.: A colored version of the \u03bb-Calculus. In: McCune, W. (ed.) 14th International Conference on Automated Deduction, pp. 291\u2013305. Springer, Heidelberg (1997); Also available as SEKI-Report SR-95- 05"},{"issue":"1-2","key":"4_CR23","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning\u00a016(1-2), 79\u2013111 (1996); Also available from Edinburgh as DAI Research Paper No 716","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/BFb0013060","volume-title":"Logic Programming and Automated Reasoning","author":"A. Ireland","year":"1992","unstructured":"Ireland, A.: The Use of Planning Critics in Mechanizing Inductive Proofs. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol.\u00a0624, pp. 178\u2013189. Springer, Heidelberg (1992); Also available from Edinburgh as DAI Research Paper 592"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_41","volume-title":"Automated Deduction - CADE-17","author":"M. Jackson","year":"2000","unstructured":"Jackson, M., Lowe, H.: XBarnacle: Making theorem provers more accessible. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, Springer, Heidelberg (2000)"},{"issue":"1-2","key":"4_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BF00244461","volume":"16","author":"I. Kraan","year":"1996","unstructured":"Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for synthesis and induction. Journal of Automated Reasoning\u00a016(1-2), 113\u2013145 (1996); Also available from Edinburgh as DAI Research Paper 729.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR27","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1007\/3-540-63104-6_39","volume-title":"14th International Conference on Automated Deduction","author":"H. Lowe","year":"1997","unstructured":"Lowe, H., Duncan, D.: XBarnacle: Making theorem provers more accessible. In: McCune, W. (ed.) 14th International Conference on Automated Deduction, pp. 404\u2013408. Springer, Heidelberg (1997)"},{"key":"4_CR28","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1017\/S0890060498124071","volume":"12","author":"H. Lowe","year":"1998","unstructured":"Lowe, H., Pechoucek, M., Bundy, A.: Proof planning for maintainable configuration systems. Artificial Intelligence in Engineering Design, Analysis and Manufacturing\u00a012, 345\u2013356 (1998); Special issue on configuration","journal-title":"Artificial Intelligence in Engineering Design, Analysis and Manufacturing"},{"key":"4_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-58216-9_29","volume-title":"Logic Programming and Automated Reasoning","author":"R. Monroy","year":"1994","unstructured":"Monroy, R., Bundy, A., Ireland, A.: Proof Plans for the Correction of False Conjectures. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol.\u00a0822, pp. 54\u201368. Springer, Heidelberg (1994); Also available from Edinburgh as DAI Research Paper 681"},{"key":"4_CR30","volume-title":"Meta-level inference: Representing and Learning Control Information in Artificial Intelligence","author":"B. Silver","year":"1985","unstructured":"Silver, B.: Meta-level inference: Representing and Learning Control Information in Artificial Intelligence. North Holland, Amsterdam (1985); Revised version of the author\u2019s PhD thesis, Department of Artificial Intelligence, U. of Edinburgh (1984)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-63263-8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Smaill","year":"1997","unstructured":"Smaill, A., Green, I.: Higher-order annotated terms for proof search. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 399\u2013414. Springer, Heidelberg (1997); Also available as DAI Research Paper 799"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48958-4_15","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Stark","year":"1999","unstructured":"Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol.\u00a01559, pp. 271\u2013288. Springer, Heidelberg (1999)"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0747-7171(89)80007-0","volume":"7","author":"L. Sterling","year":"1989","unstructured":"Sterling, L.: Bundy, Alan, Byrd, L., O\u2019Keefe, R. and Silver, B. Solving symbolic equations with PRESS. J. Symbolic Computation\u00a07, 71\u201384 (1989); Also available from Edinburgh as DAI Research Paper 171","journal-title":"J. Symbolic Computation"},{"issue":"1-2","key":"4_CR34","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0304-3975(00)00076-1","volume":"252","author":"S. Willmott","year":"2001","unstructured":"Willmott, S., Richardson, J.D.C., Bundy, A., Levine, J.M.: Applying adversarial planning techniques to Go. Journal of Theoretical Computer Science\u00a0252(1-2), 45\u201382 (2001); Special issue on algorithms, Automata, complexity and Games","journal-title":"Journal of Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30210-0_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:56:00Z","timestamp":1620014160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}