{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:27:07Z","timestamp":1748071627651},"publisher-location":"Berlin, Heidelberg","reference-count":15,"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_69","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:11Z","timestamp":1330293071000},"page":"62-76","source":"Crossref","is-referenced-by-count":12,"title":["Learning domain knowledge to improve theorem proving"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Denzinger","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"6_CR1","first-page":"62","volume":"690","author":"J. Avenhaus","year":"1993","unstructured":"Avenhaus, J.; Denzinger, J.: Distributing Equational Theorem Proving, Proc. 5th RTA, Montreal, LNCS 690, pp. 62\u201376, 1993; also available as SEKI-Report SR-93-06, University of Kaiserslautern, 1993.","journal-title":"LNCS"},{"key":"6_CR2","first-page":"397","volume":"914","author":"J. Avenhaus","year":"1995","unstructured":"Avenhaus, J.; Denzinger, J.; Fuchs, M.: DISCOUNT: A System For Distributed Equational Deduction, Proc. 6th RTA, Kaiserslautern, LNCS 914, pp. 397\u2013402, 1995.","journal-title":"LNCS"},{"key":"6_CR3","volume-title":"Completion Without Failure","author":"L. Bachmair","year":"1987","unstructured":"Bachmair, L.; Dershowitz, N.; Plaisted, D.A.: Completion Without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press, 1989."},{"key":"6_CR4","volume-title":"Internal report","author":"B.I. Dahn","year":"1994","unstructured":"Dahn, B.I.; Gehne, J.; Honigmann, T.; Walther, L.; Wolf, A.: Integrating logical Functions with ILF, Internal report, Institut f\u00fcr Reine Mathematik, Humbold-University, Berlin, 1994."},{"key":"6_CR5","first-page":"81","volume-title":"Knowledge-Based Distributed Search Using Teamwork","author":"J. Denzinger","year":"1995","unstructured":"Denzinger, J.: Knowledge-Based Distributed Search Using Teamwork, Proc. ICMAS-95, San Francisco, AAAI Press, pp. 81\u201388, 1995."},{"key":"6_CR6","first-page":"343","volume":"861","author":"J. Denzinger","year":"1994","unstructured":"Denzinger, J.; Fuchs, M.: Goal Oriented Equational Theorem Proving Using Teamwork, Proc. 18th KI-94, Saarbr\u00fccken, LNAI 861, pp. 343\u2013354, 1994; also available as SEKI-Report SR-94-04, University of Kaiserslautern, 1994.","journal-title":"LNAI"},{"key":"6_CR7","unstructured":"Denzinger, J.; Kronenburg, M.: Planning for Distributed Theorem Proving: The Teamwork Approach, SEKI-Report SR-94-09, University of Kaiserslautern, 1994."},{"key":"6_CR8","unstructured":"Denzinger, J.; Schulz, S.: Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System, SEKI-Report SR-94-05, University of Kaiserslautern, 1994."},{"key":"6_CR9","first-page":"114","volume-title":"Proc. 1st PASCO","author":"J. Denzinger","year":"1994","unstructured":"Denzinger, J.; Schulz, S.: Recording, Analyzing and Presenting Distributed Deduction Processes, Proc. 1st PASCO, Hagenberg\/Linz, pp. 114\u2013123, World Scientific Publishing, 1994."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Fuchs, M.: Learning Proof Heuristics by Adapting Parameters, Proc. 12th ML, Morgan Kaufmann, pp. 235\u2013243, 1995; also available as SEKI-Report SR-95-02, University of Kaiserslautern, 1995.","DOI":"10.1016\/B978-1-55860-377-6.50037-2"},{"key":"6_CR11","unstructured":"Fuchs, M.: Experiments in the Heuristic Use of Past Proof Experience, SEKI-report SR-95-10, University of Kaiserslautern, 1995."},{"key":"6_CR12","first-page":"54","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J.; Rusinowitch, M.: On Word Problems in Equational Theories, Proc. 14th ICALP, Karlsruhe, LNCS 267, pp. 54\u201371, 1987.","journal-title":"LNCS"},{"issue":"No.4","key":"6_CR13","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, J. of ACM 27, No. 4, pp. 798\u2013821, 1980.","journal-title":"J. of ACM"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Knuth, D.E.; Bendix, P.B.: Simple Word Problems in Universal Algebras, Computational Algebra, J. Leech, Pergamon Press, pp. 263\u2013297, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"6_CR15","first-page":"252","volume-title":"LNAI 814","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G.; Suttner, C.B.; Yemenis, T.: The TPTP Problem Library, Proc. 12th CADE, Nancy, Springer LNAI 814, pp. 252\u2013266, 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_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:20Z","timestamp":1605647240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}