{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085040},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584674"},{"type":"electronic","value":"9783540489795"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58467-6_33","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:14:11Z","timestamp":1330272851000},"page":"379-390","source":"Crossref","is-referenced-by-count":2,"title":["Adapting methods to novel tasks in proof planning"],"prefix":"10.1007","author":[{"given":"Xiaorong","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rn","family":"Richts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"33_CR1","volume-title":"Programming Expert Systems in OPS5 \u2014 An Introduction to Rule-Based Programming","author":"L. Brownston","year":"1985","unstructured":"L. Brownston, R. Farrell, E. Kant, and N. Martin. Programming Expert Systems in OPS5 \u2014 An Introduction to Rule-Based Programming. Addison-Wesley, Reading, Massachusetts, USA, 1985."},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In Proc. of 9th International Conference on Automated Deduction, pages 111\u2013120. Springer, 1988.","DOI":"10.1007\/BFb0012826"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"A. Bundy. A science of reasoning: Extended abstract. In Proc. of 10th International Conference on Automated Deduction, pages 633\u2013640. Springer, 1990.","DOI":"10.1007\/3-540-52885-7_119"},{"key":"33_CR4","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. Constable","year":"1986","unstructured":"R. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, New Jersey, 1986."},{"key":"33_CR5","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R. E. Fikes","year":"1971","unstructured":"R. E. Fikes and N. J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2:189\u2013208, 1971.","journal-title":"Artificial Intelligence"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78. Springer, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"X. Huang. Reconstructing proofs at the assertion level. In Proc. of 12th International Conference on Automated Deduction. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_53"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann. \u03a9-MKRP \u2014 a proof development environment. In Proc. of 12th International Conference on Automated Deduction. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_61"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"D. Hutter. Guiding induction proofs. In Proc. of the 10th International Conference on Automated Deduction, pages 147\u2013161. Springer, 1990.","DOI":"10.1007\/3-540-52885-7_85"},{"key":"33_CR10","volume-title":"SEKI-Report SR-93-07","author":"E. Melis","year":"1993","unstructured":"E. Melis. Change of representation in theorem proving by analogy. SEKI-Report SR-93-07, Fachbereich Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1993."},{"key":"33_CR11","unstructured":"A. Newell. The heuristic of George Polya and its relation to artificial intelligence. In R. Groner, M. Groner and W. F. Bishof, editors, Methods of Heuristics, Lawrence Erlbaum, Hillsdale, New Jersey, USA, 195\u2013243."},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"G. P\u00f3lya. How to Solve it. Princeton Univ. Press, 1945.","DOI":"10.1515\/9781400828678"},{"key":"33_CR13","volume-title":"SEKI-Report SR-93-02 (SFB)","author":"I. Sonntag","year":"1993","unstructured":"I. Sonntag and J. Denzinger. Extending automatic theorem proving by planning. SEKI-Report SR-93-02 (SFB), Fachbereich Informatik, Universit\u00e4t Kaiserslautern, Kaiserslautern, Germany, 1993."},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"K. VanLehn. Problem solving and cognitive skill acquisition. In M. I. Posner, editor, Foundations of Cognitive Science, chapter 14. MIT Press, 1989.","DOI":"10.21236\/ADA222325"}],"container-title":["Lecture Notes in Computer Science","KI-94: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58467-6_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:16:26Z","timestamp":1619572586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58467-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584674","9783540489795"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-58467-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}