{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:10:02Z","timestamp":1747548602225,"version":"3.40.5"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,11,1]],"date-time":"1998-11-01T00:00:00Z","timestamp":909878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[1998,11]]},"DOI":"10.1023\/a:1018980611571","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"299-320","source":"Crossref","is-referenced-by-count":1,"title":["Adaptation of declaratively represented methods in proof planning"],"prefix":"10.1007","volume":"23","author":[{"given":"Xiaorong","family":"Huang","sequence":"first","affiliation":[]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[]},{"given":"Lassaad","family":"Cheikhrouhou","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"325501_CR1","first-page":"281","volume-title":"Proceedings of the 5th CADE","author":"P.B. Andrews","year":"1980","unstructured":"P.B. Andrews, Transforming matings into natural deduction proofs, in: Proceedings of the 5th CADE, eds. W. Bibel and R. Kowalski, Les Arcs, France, 1980 (Springer, Berlin, 1980) pp. 281\u2013292."},{"key":"325501_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"252","volume-title":"Proceedings of the 14th CADE","author":"C. Benzm\u00fcller","year":"1997","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann and V. Sorge, \u03a9: Towards a mathematical assistant, in: Proceedings of the 14th CADE, ed. W. McCune, Townsville, Australia, 1997, Lecture Notes in Artificial Intelligence 1249 (Springer, Berlin) pp. 252\u2013255."},{"key":"325501_CR3","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland and A. Smaill, Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence 62 (1993) 185\u2013253.","journal-title":"Artificial Intelligence"},{"key":"325501_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"647","volume-title":"Proceedings of the 10th CADE","author":"A. Bundy","year":"1990","unstructured":"A. Bundy, F. van Harmelen, C. Horn and A. Smaill, The OYSTER-CLAM system, in: Proceedings of the 10th CADE, ed. M.E. Stickel, Kaiserslautern, Germany, 1990, Lecture Notes in Artificial Intelligence 449 (Springer, Berlin, 1990) pp. 647\u2013648."},{"key":"325501_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5 (1940) 56\u201368.","journal-title":"The Journal of Symbolic Logic"},{"key":"325501_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System (Prentice-Hall, Englewood Cliffs, NJ, 1986)."},{"key":"325501_CR7","series-title":"Lecture Notes in Artificial Intelligence","first-page":"16","volume-title":"Proceedings of LPAR","author":"F. Giunchiglia","year":"1994","unstructured":"F. Giunchiglia and P. Traverso, Program tactics and logic tactics, in: Proceedings of LPAR, ed. F. Pfenning, Kiev, Ukraine, 1994, Lecture Notes in Artificial Intelligence 822 (Springer, Berlin, 1994) pp. 16\u201330."},{"key":"325501_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner and C. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science 78 (Springer, Berlin, 1979)."},{"key":"325501_CR9","series-title":"Lecture Notes in Artificial Intelligence","first-page":"738","volume-title":"Proceedings of the 12th CADE","author":"X. Huang","year":"1994","unstructured":"X. Huang, Reconstructing proofs at the assertion level, in: Proceedings of the 12th CADE, ed. A. Bundy, Nancy, France, 1994, Lecture Notes in Artificial Intelligence 814 (Springer, Berlin, 1994) pp. 738\u2013752."},{"key":"325501_CR10","unstructured":"X. Huang and M. Kerber, Theorem proving as an interleaving process of planning and verification, unpublished manuscript (1991)."},{"key":"325501_CR11","series-title":"Lecture Notes in Artificial Intelligence","first-page":"788","volume-title":"Proceedings of the 12th CADE","author":"X. Huang","year":"1994","unstructured":"X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts and J. Siekmann, \u03a9-MKRP: A proof development environment, in: Proceedings of the 12th CADE, ed. A. Bundy, Nancy, 1994, Lecture Notes in Artificial Intelligence 814 (Springer, Berlin, 1994) pp. 788\u2013792."},{"key":"325501_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-58467-6_33","volume-title":"KI-94: Advances in Artificial Intelligence\u2013Proceedings of KI-94, 18th German Annual Conference on Artificial Intelligence","author":"X. Huang","year":"1994","unstructured":"X. Huang, M. Kerber, M. Kohlhase and J. Richts, Adapting methods to novel tasks in proof planning, in: KI-94: Advances in Artificial Intelligence\u2013Proceedings of KI-94, 18th German Annual Conference on Artificial Intelligence, eds. B. Nebel and L. Dreschler-Fischer, Saarbr\u00fccken, Germany, 1994, Lecture Notes in Artificial Intelligence 861 (Springer, Berlin, 1994) pp. 379\u2013390."},{"key":"325501_CR13","first-page":"277","volume":"30","author":"X. Huang","year":"1994","unstructured":"X. Huang, M. Kerber, J. Richts and A. Sehn, Planning mathematical proofs with methods, Journal of Information Processing and Cybernetics, EIK 30 (1994) 277\u2013291.","journal-title":"Journal of Information Processing and Cybernetics, EIK"},{"key":"325501_CR14","series-title":"Lecture Notes in Artificial Intelligence","first-page":"178","volume-title":"Proceedings of LPAR","author":"A. Ireland","year":"1992","unstructured":"A. Ireland, The use of planning critics in mechanizing inductive proofs, in: Proceedings of LPAR, ed. A. Voronkov, St. Petersburg, Russia, 1992, Lecture Notes in Artificial Intelligence 624 (Springer, Berlin, 1992) pp. 178\u2013189."},{"key":"325501_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/3-540-51734-0_64","volume-title":"Analogical and Inductive Inference; International Workshop AII \u201989","author":"M. Kerber","year":"1989","unstructured":"M. Kerber, Some aspects of analogy in mathematical reasoning, in: Analogical and Inductive Inference; International Workshop AII \u201989, ed. K.P. Jantke, Reinhardsbrunn Castle, GDR, October 1989, Lecture Notes in Artificial Intelligence 397 (Springer, Berlin, 1989) pp. 231\u2013242."},{"issue":"2\u20134","key":"325501_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BF02127748","volume":"18","author":"M. Kerber","year":"1996","unstructured":"M. Kerber and A. Pr\u00e4cklein, Using tactics to reformulate formulae for resolution theorem proving, Annals of Mathematics and Artificial Intelligence 18(2\u20134) (1996) 221\u2013241.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"3","key":"325501_CR17","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"W. McCune, Solution of the Robbins problem, Journal of Automated Reasoning 19(3) (1997) 263\u2013276. See also http:\/\/www.mcs.anl.gov\/home\/mccune\/ar\/robbins\/.","journal-title":"Journal of Automated Reasoning"},{"key":"325501_CR18","series-title":"Technical Report","volume-title":"Representing and reformulating diagonalization methods","author":"E. Melis","year":"1994","unstructured":"E. Melis, Representing and reformulating diagonalization methods, Technical Report CMU-CS-94-174, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA (1994)."},{"key":"325501_CR19","first-page":"47","volume":"1","author":"T.M. Mitchell","year":"1986","unstructured":"T.M. Mitchell, R.M. Keller and S.T. Kedar-Cabelli, Explanation-based generalization: A unifying view, Machine Learning 1 (1986) 47\u201380.","journal-title":"Machine Learning"},{"key":"325501_CR20","doi-asserted-by":"crossref","DOI":"10.1515\/9781400828678","volume-title":"How to Solve It","author":"G. P\u00f3lya","year":"1945","unstructured":"G. P\u00f3lya, How to Solve It(Princeton University Press, Princeton, NJ, 1945; Penguin Book, London, 1990)."},{"key":"325501_CR21","volume-title":"Foundations of Cognitive Science","author":"K. VanLehn","year":"1989","unstructured":"K. VanLehn, Problem solving and cognitive skill acquisition, in: Foundations of Cognitive Science, ed. M.I. Posner (MIT Press, Cambridge, MA, 1989) chapter 14."},{"key":"325501_CR22","volume-title":"Automated Reasoning\u2013Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"L. Wos, R. Overbeek, E. Lusk and J. Boyle, Automated Reasoning\u2013Introduction and Applications (Prentice-Hall, Englewood Cliffs, NJ, 1984)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018980611571.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018980611571\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018980611571.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:31:20Z","timestamp":1747546280000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018980611571"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,11]]},"references-count":22,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1998,11]]}},"alternative-id":["325501"],"URL":"https:\/\/doi.org\/10.1023\/a:1018980611571","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[1998,11]]}}}