{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:31Z","timestamp":1725664231083},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_72","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:19Z","timestamp":1330293079000},"page":"106-120","source":"Crossref","is-referenced-by-count":3,"title":["Termination of theorem proving by reuse"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Kolbe","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Walther","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"9_CR1","volume-title":"Spike: An Automatic Theorem Prover","author":"A. Bouhoula","year":"1992","unstructured":"A. Bouhoula, E. Kounalis, and M. Rusinowitch. Spike: An Automatic Theorem Prover. In Proceedings of the Conference on Logic Programming and Automated Reasoning (LPAR-92), St. Petersburg, Russia. Springer, 1992."},{"key":"9_CR2","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979."},{"key":"9_CR3","unstructured":"J. Brauburger. Plagiator \u2014 Design and Implementation of a Learning Theorem Prover. Diploma Thesis, TH Darmstadt, 1994. (in German)."},{"issue":"1","key":"9_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1,2):69\u2013115, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite Systems, volume B of the Handbook of Theoretical Computer Science: Formal Models and Semantics, chapter 6, pages 243\u2013320. Elsevier Science Publishers B.V., 1990. Jan van Leeuwen (Ed.).","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"8","key":"9_CR6","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM, 22(8):465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"issue":"2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/66443.66445","volume":"21","author":"T. Ellman","year":"1989","unstructured":"T. Ellman. Explanation-Based Learning: A Survey of Programs and Perspectives. ACM Computing Surveys, 21(2):163\u2013221, 1989.","journal-title":"ACM Computing Surveys"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F. Giunchiglia","year":"1992","unstructured":"F. Giunchiglia and T. Walsh. A Theory of Abstraction. Artificial Intelligence, 57:323\u2013389, 1992.","journal-title":"Artificial Intelligence"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/0004-3702(89)90003-9","volume":"39","author":"R. P. Hall","year":"1989","unstructured":"R. P. Hall. Computational Approaches to Analogical Reasoning: A Comparative Analysis. Artificial Intelligence, 39:39\u2013120, 1989.","journal-title":"Artificial Intelligence"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"A. Ireland and A. Bundy. Productive Use of Failure in Inductive Proof. Special Issue of the Journal of Automated Reasoning on Automation of Proofs by Mathematical Induction, 1996.","DOI":"10.1007\/978-94-009-1675-3_3"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"D. Kapur and H. Zhang. RRL: A Rewrite Rule Laborarory. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction (CADE-88), Argonne, pages 768\u2013769. Springer LNCS 310, 1988.","DOI":"10.1007\/BFb0012889"},{"key":"9_CR12","first-page":"80","volume-title":"Reusing Proofs","author":"T. Kolbe","year":"1994","unstructured":"T. Kolbe and C. Walther. Reusing Proofs. In A. Cohn, editor, Proceedings of the 11th European Conference on Artificial Intelligence (ECAI-94), Amsterdam, The Netherlands, pages 80\u201384. John Wiley & Sons, Ltd., 1994."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"T. Kolbe and C. Walther. Patching Proofs for Reuse. In N. Lavrac and S. Wrobel, editors, Proceedings of the European Conference on Machine Learning (ECML-95), Heraklion, Greece, pages 303\u2013306. Springer LNAI 912, 1995.","DOI":"10.1007\/3-540-59286-5_73"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"T. Kolbe and C. Walther. Patching Proofs for Reuse. Technical Report IBN 95\/27, Technische Hochschule Darmstadt, 1995.","DOI":"10.1007\/3-540-59286-5_73"},{"key":"9_CR15","unstructured":"T. Kolbe and C. Walther. Proof Management and Retrieval. In Proceedings of the IJCAI'95 Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs, pages 16\u201320, 1995."},{"key":"9_CR16","unstructured":"T. Kolbe and C. Walther. Second-Order Matching modulo Evaluation \u2014 A Technique for Reusing Proofs. In Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI-95), Montreal, Canada, pages 190\u2013195, 1995."},{"key":"9_CR17","unstructured":"T. Kolbe and C. Walther. On the Benefits of Reusing Past Problem Solutions. Technical Report IBN 96\/35, Technische Hochschule Darmstadt, 1996."},{"key":"9_CR18","volume-title":"Problem Solving Methods in Artificial Intelligence","author":"N. J. Nilsson","year":"1971","unstructured":"N. J. Nilsson. Problem Solving Methods in Artificial Intelligence. McGraw Hill, New York, 1971."},{"key":"9_CR19","unstructured":"C. Walther. Mathematical Induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 127\u2013227. Oxford University Press, 1994."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_72.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:21Z","timestamp":1605647241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_72"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_72","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}