{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:56Z","timestamp":1725485576135},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_23","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:48:36Z","timestamp":1180651716000},"page":"337-351","source":"Crossref","is-referenced-by-count":1,"title":["A Semantics for Proof Plans with Applications to Interactive Proof Planning"],"prefix":"10.1007","author":[{"given":"Julian","family":"Richardson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Serge Autexier Axel Schairer and Dieter Hutter. A pragmatic approach to reuse in tactical theorem proving. In Maria Paola Bonacina and Bernhard Gramlich, editors, Electronic Notes in Theoretical Computer Science, volume 58. Elsevier Science Publishers, 2001.","DOI":"10.1016\/S1571-0661(04)00286-5"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D Fehrer, A. Fiedler, X. Huang, M. Kerber, K. Kohlhase, A Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge. \u03a9mega: Towards a mathematical assistant. In W. McCune, editor, 14 th International Conference on Automated Deduction, pages 252\u2013255. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"23_CR3","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. Earlier version available from Edinburgh as DAI Research Paper No 413.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Arie de Bruin and Erik P. de Vink. Continuation semantics for PROLOG with cut. In TAPSOFT, Vol.1, pages 178\u2013192, 1989.","DOI":"10.1007\/3-540-50939-9_132"},{"key":"23_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF-A mechanised logic of computation","author":"M. J. Gordon","year":"1979","unstructured":"M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF-A mechanised logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"issue":"1-2","key":"23_CR6","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-2):79\u2013111, 1996. Also available from Edinburgh as DAI Research Paper No 716.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR7","unstructured":"M. Jamnik, M. Kerber, and M. Pollet. Automatic learning in proof planning. In F. van Harmelen, editor, Proceedings of 15th ECAI. European Conference on Artificial Intelligence. Springer Verlag, Forthcoming."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Richard B. Kieburtz. A logic for rewriting strategies. In Maria Paola Bonacina and Bernhard Gramlich, editors, Electronic Notes in Theoretical Computer Science, volume 58. Elsevier Science Publishers, 2001.","DOI":"10.1016\/S1571-0661(04)00283-X"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"D. Lacey, J. D. C. Richardson, and A. Smaill. Logic program synthesis in a higher order setting. In Proceedings of the First International Conference on Computational Logic (CL2000), volume 1861 of Lecture Notes in AI, pages 912\u2013925. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44957-4_6"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"H. Lowe and D. Duncan. XBarnacle: Making theorem provers more accessible. In William McCune, editor, 14th International Conference on Automated Deduction, pages 404\u2013408. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_39"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 1999.","DOI":"10.1016\/S0004-3702(99)00076-4"},{"key":"23_CR12","series-title":"Technical Report DII 11\/01","volume-title":"International Joint Conference on Automated Reasoning, IJCAR-2001-Short Papers","author":"J. D. C. Richardson","year":"2001","unstructured":"J. D. C. Richardson and A. Smaill. Continuations of proof strategies. In International Joint Conference on Automated Reasoning, IJCAR-2001-Short Papers, June 2001. Technical Report DII 11\/01, Dipartimento di Ingegneria dell\u2019Informazione, Universit\u00e0 di Siena, Italy."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"J. D. C Richardson, A. Smaill, and I. M. Green. System description: proof planning in higher-order logic with IClam. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, editors, 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Artificial Intelligence, Lindau, Germany, July 1998.","DOI":"10.1007\/BFb0054254"},{"key":"23_CR14","first-page":"1","volume":"3","author":"J. Siekmann","year":"1999","unstructured":"J. Siekmann, S. Hess, C. Benzmueller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, and V. Sorge. Loui: Lovely Omegauser interface. Formal Aspects of Computing, 3:1\u201318, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"23_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Stratego: A language for program transformation based on rewriting strategies","author":"E. Visser","year":"2001","unstructured":"Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. Lecture Notes in Computer Science volume 2051, 2001."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:18:11Z","timestamp":1556450291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}