{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:24:11Z","timestamp":1743009851014,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142024"},{"type":"electronic","value":"9783642142031"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14203-1_37","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T13:10:58Z","timestamp":1278940258000},"page":"434-440","source":"Crossref","is-referenced-by-count":0,"title":["Premise Selection in the Naproche System"],"prefix":"10.1007","author":[{"given":"Marcos","family":"Cramer","sequence":"first","affiliation":[]},{"given":"Peter","family":"Koepke","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"K\u00fchlwein","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"37_CR1","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF02341853","volume":"8","author":"D. Barker-Plummer","year":"1992","unstructured":"Barker-Plummer, D.: Gazing: An Approach to the Problem of Definition and Lemma Use. J. Autom. Reasoning\u00a08(3), 311\u2013344 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"37_CR2","series-title":"Cognitive Technologies Series","volume-title":"Resource Adaptive Cognitive Processes","author":"C. Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Schiller, M., Siekmann, J.: Resource-bounded modelling and analysis of human-level interactive proofs. In: Crocker, M., Siekmann, J. (eds.) Resource Adaptive Cognitive Processes. Cognitive Technologies Series. Springer, Heidelberg (2010) (in print)"},{"key":"37_CR3","doi-asserted-by":"crossref","unstructured":"Cramer, M., Fisseni, B., Koepke, P., K\u00fchlwein, D., Schr\u00f6der, B., Veldman, J.: The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009 Workshop. LNCS, vol.\u00a05972, pp. 170\u2013186. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14418-9_11"},{"key":"37_CR4","unstructured":"Cramer, M.: Mathematisch-logische Aspekte von Beweisrepresentationsstrukturen. Master\u2019s thesis, University of Bonn (2009)"},{"key":"37_CR5","unstructured":"Koepke, P., K\u00fchlwein, D., Cramer, M., Schr\u00f6der, B.: The Naproche System (2009)"},{"key":"37_CR6","unstructured":"Ganesalingam, M.: The Language of Mathematics. PhD thesis, University of Cambridge (2009)"},{"key":"37_CR7","unstructured":"Heath, T.L., Euclid: The Thirteen Books of Euclid\u2019s Elements, Books 1 and 2. Dover Publications, New York (1956) (Incorporated)"},{"key":"37_CR8","unstructured":"Hoder, K.: Automated Reasoning in Large Knowledge Bases. Master\u2019s thesis, Charles University (2008)"},{"key":"37_CR9","unstructured":"Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"37_CR10","unstructured":"Kuehlwein, D.: A Calculus for Proof Representation Structures. Master\u2019s thesis, University of Bonn (2008)"},{"key":"37_CR11","unstructured":"Landau, E.: Grundlagen der Analysis. Chelsea Publishing Company (1930)"},{"key":"37_CR12","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications\u00a04 (2005)"},{"issue":"1","key":"37_CR13","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"2\/3","key":"37_CR15","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"issue":"4","key":"37_CR16","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"37_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - A Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"key":"37_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vyskocil, J.: MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"37_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-73595-3_29","volume-title":"Automated Deduction \u2013 CADE-21","author":"K. Verchinine","year":"2007","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A.: System for Automated Deduction (SAD): A Tool for Proof Verification. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 398\u2013403. Springer, Heidelberg (2007)"},{"issue":"3","key":"37_CR20","first-page":"120","volume":"7","author":"K. Vershinin","year":"2000","unstructured":"Vershinin, K., Paskevich, A.: ForTheL - the language of formal theories. International Journal of Information Theories and Applications\u00a07(3), 120\u2013126 (2000)","journal-title":"International Journal of Information Theories and Applications"},{"key":"37_CR21","unstructured":"Wenzel, M.: Isabelle\/Isar - a generic framework for human-readable proof documents. Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23). University of Bia\u0142ystok (2007)"},{"issue":"4","key":"37_CR22","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/BF00247438","volume":"3","author":"L. Wos","year":"1987","unstructured":"Wos, L.: The problem of definition expansion and contraction. J. Autom. Reason.\u00a03(4), 433\u2013435 (1987)","journal-title":"J. Autom. Reason."},{"key":"37_CR23","unstructured":"Zinn, C.: Understanding Informal Mathematical Discourse. PhD thesis, Friedrich-Alexander-Universitt Erlangen N\u00fcrnberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14203-1_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,20]],"date-time":"2021-08-20T02:03:47Z","timestamp":1629425027000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14203-1_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142024","9783642142031"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14203-1_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}