{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:40Z","timestamp":1725664240343},"publisher-location":"Berlin, Heidelberg","reference-count":18,"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_111","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:51:08Z","timestamp":1330275068000},"page":"523-537","source":"Crossref","is-referenced-by-count":10,"title":["Experiments in the heuristic use of past proof experience"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"48_CR1","first-page":"62","volume":"690","author":"J. Avenhaus","year":"1993","unstructured":"Avenhaus, J.; Denzinger, J.: Distributing equational theorem proving, Proc. 5th RTA, Montreal, CAN, 1993, LNCS 690, pp. 62\u201376","journal-title":"LNCS"},{"key":"48_CR2","first-page":"454","volume":"310","author":"B. Brock","year":"1988","unstructured":"Brock, B.; Cooper, S.; Pierce, W.: Analogical reasoning and proof discovery, Proc. CADE 9, Argonne, IL, USA, 1988, LNCS 310, pp. 454\u2013468","journal-title":"LNCS"},{"key":"48_CR3","unstructured":"Denzinger, J.:Knowledge-Based. Distributed Search Using Teamwork, Proc. 1stth ICMAS, San Francisco, CA, USA, 1995, pp. 81\u201388"},{"key":"48_CR4","doi-asserted-by":"crossref","unstructured":"Fuchs, M.:Learning proof heuristics by adapting parameters, Proc. 12th ICML, Tahoe City, CA, USA, 1995, pp. 235\u2013243","DOI":"10.1016\/B978-1-55860-377-6.50037-2"},{"key":"48_CR5","unstructured":"Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, SEKI-Report SR-95-10, University of Kaiserslautern, 1995, obtainable via WWW at the URL http: \/\/www.uni-kl.de\/AG-AvenhausMadlener\/fuchs.html"},{"key":"48_CR6","unstructured":"Fuchs, M.:Powerful Search Heuristics Based on Weighted Symbols, Level and Features, Proc. FLAIRS '96, Key West, FL, USA, 1996"},{"key":"48_CR7","unstructured":"Koehler, J.; Nebel, B.:Plan modification versus plan generation, Proc. IJ-CAI '93, Chambery, FRA, 1993, pp. 1436\u20131444"},{"key":"48_CR8","first-page":"80","volume-title":"Proc. 11th ECAI '94","author":"T. Kolbe","year":"1994","unstructured":"Kolbe, T.; Walther, C.: Reusing proofs, Proc. 11th ECAI '94, Amsterdam, HOL, 1994, pp. 80\u201384"},{"key":"48_CR9","volume-title":"Proc. 8th ECML '95","author":"T. Kolbe","year":"1995","unstructured":"Kolbe, T.; Walther, C.: Patching Proofs for Reuse, Proc. 8th ECML '95, Heraklion, Crete\/Greece, 1995"},{"key":"48_CR10","unstructured":"\u0141ukasiewicz, J.:Selected Works, L. Borkowski (ed.), North-Holland, 1970"},{"key":"48_CR11","first-page":"209","volume":"607","author":"W. McCune","year":"1992","unstructured":"McCune, W.; Wos, L.: Experiments in Automated Deduction with Condensed Detachment, Proc. CADE 11, Saratoga Springs, NY, USA, 1992, LNAI 607, pp. 209\u2013223","journal-title":"LNAI"},{"key":"48_CR12","first-page":"470","volume":"449","author":"C. Suttner","year":"1990","unstructured":"Suttner, C.; Ertel, W.: Automatic acquisition of search-guiding heuristics, Proc. CADE 10, Kaiserslautern, FRG, 1990, LNAI 449, pp. 470\u2013484","journal-title":"LNAI"},{"issue":"Nr.2","key":"48_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/362515.362560","volume":"14","author":"J.R. Slagle","year":"1971","unstructured":"Slagle, J.R.; Farrell, C.D.: Experiments in automatic learning for a multipurpose heuristic program, Communications of the ACM, Vol. 14, Nr. 2, 1971, pp. 91\u201399","journal-title":"Communications of the ACM"},{"key":"48_CR14","unstructured":"Slaney, J.:SCOTT: A Model-Guided Theorem Prover, Proc. IJCAI '93, Chambery, FRA, 1993, pp. 109\u2013114"},{"key":"48_CR15","first-page":"252","volume":"814","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G.; Suttner, C.; Yemenis, T.: The TPTP Problem Library, Proc. CADE-12, Nancy, FRA, 1994, LNAI 814, pp. 252\u2013266","journal-title":"LNAI"},{"key":"48_CR16","unstructured":"Tarski, A.:Logic, Semantics, Metamathematics, Oxford University Press, 1956"},{"key":"48_CR17","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00245821","volume":"6","author":"L. Wos","year":"1990","unstructured":"Wos, L.: Meeting the Challenge of Fifty Years of Logic, JAR 6, 1990, pp. 213\u2013232","journal-title":"JAR"},{"key":"48_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF00881802","volume":"15","author":"L. Wos","year":"1995","unstructured":"Wos, L.: Searching for Circles of Pure Proofs, JAR 15, 1995, pp. 279\u2013315","journal-title":"JAR"}],"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_111.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:33:34Z","timestamp":1619559214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_111"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_111","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}