{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:36Z","timestamp":1725475896677},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_33","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"431-435","source":"Crossref","is-referenced-by-count":0,"title":["Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO"],"prefix":"10.1007","author":[{"given":"Joachim","family":"Draeger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"O. Astrachan","year":"1992","unstructured":"Astrachan, O., Stickel, M.: Caching and Lemmaizing in Model Elimination Theorem Provers. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, Springer. Heidelberg (1992)"},{"key":"33_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/BFb0057448","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"J. Draeger","year":"1998","unstructured":"Draeger, J.: Acquisition of Useful Lemma Knowledge in Automated Reasoning. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol.\u00a01480, p. 230. Springer, Heidelberg (1998)"},{"key":"33_CR3","unstructured":"Draeger, J.: Modularisierte Suche in Theorembeweisern. Ph.D. Dissertation, Technical University Munich (1998)"},{"key":"33_CR4","unstructured":"Draeger, J., Wolf, A.: Strategy Parallelism and Lemma Evaluation. In: FLAIRS 1999 (1999)"},{"key":"33_CR5","unstructured":"5. Goller, C.: A Connectionist Approach for Learning Search-Control Heuristics for Automated Deduction Systems, Ph.D. Dissertation, Technical University Munich (1997)"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","author":"C. Goller","year":"1994","unstructured":"Goller, C., Letz, R., Mayr, K., Schumann, J.: SETHEO V3.2: Recent Developments. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Loveland, D.: Mechanical Theorem-Proving by Model Elimination. JACM\u00a015(2) (1968)","DOI":"10.1145\/321450.321456"},{"key":"33_CR8","volume-title":"Automated Theorem Proving: a Logical Basis","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.: Automated Theorem Proving: a Logical Basis. North-Holland, Amsterdam (1978)"},{"key":"33_CR9","unstructured":"Mitchell, T.: Learning and Problem Solving. In: IJCAI (1983)"},{"issue":"2","key":"33_CR10","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., et al.: SETHEO and E-SETHEO. The CADE-13 Systems. JAR\u00a018(2), 237 (1997)","journal-title":"JAR"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","author":"J. Schumann","year":"1994","unstructured":"Schumann, J.: DELTA A Bottom-up Preprocessor for Top-Down Theorem Provers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP Problem Library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"33_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/3-540-48754-9_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Wolf","year":"1999","unstructured":"Wolf, A., Draeger, J.: Strategy Parallelism and Lemma Evaluation. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 319\u2013323. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T09:38:46Z","timestamp":1553333926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/10722086_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}