{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T19:40:04Z","timestamp":1736106004541,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635864"},{"type":"electronic","value":"9783540696056"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0023907","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T07:20:36Z","timestamp":1132384836000},"page":"13-24","source":"Crossref","is-referenced-by-count":1,"title":["Flexible re-enactment of proofs"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,10]]},"reference":[{"key":"2_CR1","unstructured":"Bachmair, L.; Dershowitz, N.; Plaisted, D.:Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin, TX, USA (1987), Academic Press, 1989."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Brock, B.; Cooper, 5.; Pierce, W.:Analogical Reasoning and Proof Discovery, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 454\u2013468.","DOI":"10.1007\/BFb0012849"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bundy, A.:The Use of Explicit Plans to Guide Inductive Proofs, Proc. CADE-9, Argonne, IL, USA, 1988, Springer LNCS 310, pp. 111\u2013120.","DOI":"10.1007\/BFb0012826"},{"key":"2_CR4","unstructured":"Chang, C.L.; Lee, R.C.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"key":"2_CR5","unstructured":"Denzinger, J.; Fuchs, M.; Fuchs, Marc:High Performance ATP Systems by Combining Several AI Methods, SEKI Report SR-96-09, University of Kaiserslautern, 1996, http:\/\/www.uni-kl.de\/AG-AvenhausMadlener\/fuchs.html."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Denzinger, J.; Schulz, S.:Learning Domain Knowledge to Improve Theorem Proving, Proc. LADE-13, New Brunswick, NJ, USA, 1996, Springer LNAI 1104, pp. 62\u201376.","DOI":"10.1007\/3-540-61511-3_69"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Fuchs, D.; Fuchs, M.:CODE: A Powerful Prover for Problems of Condensed Detachment, Proc. LADE-14, Townsville, AUS, 1997, Springer LNAI, to appear.","DOI":"10.1007\/3-540-63104-6_25"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Fuchs, M.:Learning Proof Heuristics by Adapting Parameters, Proc. 12th ICML, Tahoe City, CA, USA, 1995, Morgan Kaufmann, pp. 235\u2013243.","DOI":"10.1016\/B978-1-55860-377-6.50037-2"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, SEKI Report SR-95-10, University of Kaiserslautern, 1996, obtainable via WWW at http:\/\/www.uni-kl.de\/AG-AvenhausMadlener\/fuchs.html.","DOI":"10.1007\/3-540-61511-3_111"},{"key":"2_CR10","unstructured":"Fuchs, M.:Powerful Search Heuristics Based on Weighted Symbols, Level, and Features, Proc. FLAIRS-96, Key West, FL, USA, 1996, pp. 449\u2013453."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Fuchs, M.:Experiments in the Heuristic Use of Past Proof Experience, Proc. CADS-13, New Brunswick, NJ, USA, 1996, Springer LNAI 1104, pp. 523\u2013537.","DOI":"10.1007\/3-540-61511-3_111"},{"key":"2_CR12","unstructured":"Fuchs, M.:Towards Full Automation of Deduction: A Case Study, SEKI Report SR-96-07, University of Kaiserslautern, 1996, obtainable via WWW at http:\/\/www.uni-kl.de\/AG-AvenhausMadlener\/fuchs.html."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Fuchs, M.:Flexible Re-enactment of Proofs, SEKI Report SR-97-O1, Univ. of Kaiserslautern,1997,http:\/\/www.uni-kl.de\/AG-AvenhausMadlener\/fuchs.html.","DOI":"10.1007\/BFb0023907"},{"key":"2_CR14","unstructured":"Kolbe, T.; Walther, C.:Reusing Proofs, Proc. 11th ECAI '94, Amsterdam, HOL, 1994, pp. 80\u201384."},{"key":"2_CR15","unstructured":"Lukasiewicz, J.:Selected Works, L. Borkowski (ed.), North-Holland, 1970."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"McCune, W.; Wos, L.:Experiments in Automated Deduction with Condensed Detachment, Proc. LADE-11, Saratoga Springs, NY, USA, 1992, Springer LNAI 607, pp. 209\u2013223.","DOI":"10.1007\/3-540-55602-8_167"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"McCune, W.:OTTER 3.0 reference manual and guide, Techn. report ANL-946, Argonne Natl. Laboratory, 1994.","DOI":"10.2172\/10129052"},{"key":"2_CR18","unstructured":"Melis, E.:A Model of Analogy-driven Proof-plan Construction, Proc. 14th IJCAI, Montreal, CAN, AAAl Press, 1995, pp. 182\u2013189."},{"issue":"1","key":"2_CR19","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1305\/ndjfl\/1093888213","volume":"19","author":"G.J. Peterson","year":"1976","unstructured":"Peterson, G.J.: An Automatic Theorem Prover for Substitution and Detachment Systems, Notre Dame J. of Formal Logic, Vol. 19, No. 1, Jan. 1976, pp. 119\u2013122.","journal-title":"Notre Dame J. of Formal Logic"},{"issue":"2","key":"2_CR20","doi-asserted-by":"crossref","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 of a Multipurpose Heuristic Program, Comm. of the ACM, Vol. 14, No. 2, 1971, pp. 91\u201399.","journal-title":"Comm. of the ACM"},{"key":"2_CR21","unstructured":"Slaney, J.:SCOTT: A Model-guided Theorem Prover, Proc. IJCAI'93, Chambery, FRA, 1993, AAAI Press, pp. 109\u2013114."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.; Suttner, C.; Yemenis, T.:The TPTP Problem Library, Proc. LADE-12, Nancy, FRA, 1994, Springer LNAI 814, pp. 252\u2013266.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Suttner, C.; Ertel, W.:Automatic Acquisition of Search-guiding Heuristics, Proc. CADE-10, Kaiserslautern, FRG, 1990, Springer LNAI 449, pp. 470\u2013484.","DOI":"10.1007\/3-540-52885-7_108"},{"key":"2_CR24","unstructured":"Tarski, A.:Logic, Semantics, Metamathematics, Oxford University Press, 1956."},{"key":"2_CR25","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R. Veroff","year":"1996","unstructured":"Veroff, R.:, Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies, JAR 16:223\u2013239, 1996.","journal-title":"JAR"},{"key":"2_CR26","doi-asserted-by":"crossref","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:213\u2013232, 1990.","journal-title":"JAR"},{"key":"2_CR27","doi-asserted-by":"crossref","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:279\u2013315, 1995.","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023907","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T18:58:32Z","timestamp":1736103512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635864","9783540696056"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0023907","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}