{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:34:37Z","timestamp":1743136477583,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:04:38Z","timestamp":1330297478000},"page":"256-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Plagiator \u2014 A learning prover"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Kolbe","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Brauburger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"24_CR1","volume-title":"Proc. CADE-14","author":"C. Benzm\u00fcller","year":"1997","unstructured":"C. Benzm\u00fcller et. al. OMEGA: Towards a Mathematical Assistant. In Proc. CADE-14, Townsville, Australia. Springer 1997."},{"key":"24_CR2","unstructured":"J. Brauburger. Plagiator \u2014 Design and Implementation of a Learning Prover. Diploma Thesis (in German), TH Darmstadt, 1994."},{"key":"24_CR3","first-page":"136","volume":"1104","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia and A. Villafiorita. ABSFOL: A Proof Checker with Abstraction. In Proc. CADE-13, New Brunswick, USA, pp. 136\u2013140. Springer LNAI 1104, 1996.","journal-title":"Springer LNAI"},{"key":"24_CR4","first-page":"288","volume":"1104","author":"D. Hutter","year":"1996","unstructured":"D. Hutter and C. Sengler. INKA: The Next Generation. In Proc. CADE-13, New Brunswick, USA, pp. 288\u2013292. Springer LNAI 1104, 1996.","journal-title":"Springer LNAI"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"T. Kolbe and S. Glesner. Many-Sorted Logic in a Learning Theorem Prover. Technical Report IBN 97\/43, TH Darmstadt, 1997.","DOI":"10.1007\/3540634932_5"},{"key":"24_CR6","first-page":"80","volume-title":"Proc. ECAI-11","author":"T. Kolbe","year":"1994","unstructured":"T. Kolbe and C. Walther. Reusing Proofs. In A. Cohn, editor, Proc. ECAI-11, Amsterdam, The Netherlands, pp. 80\u201384. John Wiley & Sons, Ltd., 1994."},{"key":"24_CR7","unstructured":"T. Kolbe and C. Walther. Proof Management and Retrieval. In Proceedings of the IJCAI-14 Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs, Montreal, Canada, pp. 16\u201320, 1995."},{"key":"24_CR8","unstructured":"T. Kolbe and C. Walther. Second-Order Matching modulo Evaluation \u2014 A Technique for Reusing Proofs. In Proc. IJCAI-14, Montreal, Canada, pp. 190\u2013195, 1995."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"T. Kolbe and C. Walther. Termination of Theorem Proving by Reuse. In Proc. CADE-13, New Brunswick, USA, pp. 106\u2013120. Springer LNAI 1104, 1996.","DOI":"10.1007\/3-540-61511-3_72"},{"key":"24_CR10","volume-title":"Proc. CADE-14","author":"W. Reif","year":"1997","unstructured":"W. Reif, G. Schellhorn and K. Stenzel. Proving System Correctness with KIV 3.0. In Proc. CADE-14, Townsville, Australia. Springer 1997."},{"key":"24_CR11","doi-asserted-by":"crossref","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, pp. 127\u2013227. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198537465.003.0003"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T18:02:39Z","timestamp":1713636159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}