{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:20Z","timestamp":1771059800139,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405597","type":"print"},{"value":"9783540450856","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_22","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"279-283","source":"Crossref","is-referenced-by-count":46,"title":["IsaPlanner: A Prototype Proof Planner in Isabelle"],"prefix":"10.1007","author":[{"given":"Lucas","family":"Dixon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"LNAI","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 (LNAI), vol.\u00a01479, pp. 87\u2013104. Springer, Heidelberg (1998)"},{"key":"22_CR2","series-title":"ACM monograph series","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM monograph series. Academic Press, London (1979)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning\u00a07, 303\u2013324 (1991)","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/BFb0031802","volume-title":"Formal Methods in Computer-Aided Design","author":"F. Cantu","year":"1996","unstructured":"Cantu, F., Bundy, A., Smaill, A., Basin, D.: Experiments in automating hardware verification using inductive proof planning. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 94\u2013108. Springer, Heidelberg (1996)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-44755-5_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L.A. Dennis","year":"2001","unstructured":"Dennis, L.A., Smaill, A.: Ordinal arithmetic: A case study for rippling in a higher order domain. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 185\u2013200. Springer, Heidelberg (2001)"},{"issue":"1\u20132","key":"22_CR6","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\u20132), 79\u2013111 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-44957-4_6","volume-title":"Computational Logic - CL 2000","author":"D. Lacey","year":"2000","unstructured":"Lacey, D., Richardson, J.D.C., Smaill, A.: Logic program synthesis in a higher order setting. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS, vol.\u00a01861, pp. 87\u2013100. Springer, Heidelberg (2000)"},{"key":"22_CR8","unstructured":"Maclean, E., Fleuriot, J., Smaill, A.: Proof-planning non-standard analysis. In: The 7th International Symposium on AI and Mathematics (2002)"},{"issue":"1","key":"22_CR9","first-page":"65","volume":"115","author":"E. Mellis","year":"1999","unstructured":"Mellis, E., Siekmann, J.H.: Knowledge-based proof planning. Journal of AI\u00a0115(1), 65\u2013105 (1999)","journal-title":"Journal of AI"},{"key":"22_CR10","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science\u00a05(3) (1999)"},{"key":"22_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A generic theorem prover. Springer, Heidelberg (1994)"},{"key":"22_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Automated Deduction - CADE-15","author":"J.D.C. Richardson","year":"1998","unstructured":"Richardson, J.D.C., Smaill, A., Green, I.: System description: proof planning in higher-order logic with Lambda-Clam. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 129\u2013133. Springer, Heidelberg (1998)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0028400","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1997","unstructured":"Slind, K.: Derivation and use of induction schemes in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 275\u2013290. Springer, Heidelberg (1997)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T21:54:34Z","timestamp":1553205274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}