{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:34:15Z","timestamp":1725838455388},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_23","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"329-339","source":"Crossref","is-referenced-by-count":3,"title":["There Is No Best $$\\beta $$ -Normalization Strategy for Higher-Order Reasoners"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Steen","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., Levy, J.J.: Explicit substitutions. In: Proceedings of the 17th Symposium on Principles of Programming Languages, POPL 1990, pp. 31\u201346. ACM, New York, NY, USA (1990)","DOI":"10.1145\/96709.96712"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-45221-5_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Raths, T.: HOL based first-order modal logic provers. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 127\u2013136. Springer, Heidelberg (2013)"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"NGD Bruijn","year":"1972","unstructured":"Bruijn, N.G.D.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. MATH 34, 381\u2013392 (1972)","journal-title":"INDAG. MATH"},{"issue":"5","key":"23_CR4","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Logic Comput. 13(5), 639\u2013688 (2003)","journal-title":"J. Logic Comput."},{"issue":"2","key":"23_CR5","doi-asserted-by":"publisher","first-page":"346","DOI":"10.2307\/1968337","volume":"33","author":"A Church","year":"1932","unstructured":"Church, A.: A set of postulates for the foundation of logic. Ann. Math. 33(2), 346\u2013366 (1932)","journal-title":"Ann. Math."},{"issue":"4","key":"23_CR6","doi-asserted-by":"publisher","first-page":"839","DOI":"10.2307\/1968702","volume":"34","author":"A Church","year":"1933","unstructured":"Church, A.: A set of postulates for the foundation of logic. Second Paper. Ann. Math. 34(4), 839\u2013864 (1933)","journal-title":"Second Paper. Ann. Math."},{"issue":"2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-71070-7_13","volume-title":"Automated Reasoning","author":"A Gacek","year":"2008","unstructured":"Gacek, A.: The abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154\u2013161. Springer, Heidelberg (2008)"},{"key":"23_CR9","unstructured":"Girard, J.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII (1972)"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10817-004-6885-1","volume":"33","author":"C Liang","year":"2004","unstructured":"Liang, C., Nadathur, G., Qi, X.: Choices in representation and reduction strategies for lambda terms in intensional contexts. J. Autom. Reasoning 33(2), 89\u2013132 (2004)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"23_CR11","first-page":"1","volume":"1999","author":"G Nadathur","year":"1999","unstructured":"Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations. J. Funct. Logic Program. 1999(2), 1\u201362 (1999)","journal-title":"J. Funct. Logic Program."},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Automated Deduction - CADE-16","author":"G Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: teyjus - a compiler and abstract machine based implementation of \n                    \n                      \n                    \n                    $$\\lambda $$\n                  prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287\u2013291. Springer, Heidelberg (1999)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning","author":"B Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-31365-3_35","volume-title":"Automated Reasoning","author":"T Raths","year":"2012","unstructured":"Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 454\u2013461. Springer, Heidelberg (2012)"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Symposium on Programming","author":"JC Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Symposium on Programming. LNCS, vol. 19, pp. 408\u2013423. Springer, Heidelberg (1974)"},{"key":"23_CR17","unstructured":"Reynolds, J.C.: An introduction to polymorphic lambda calculus. In: Logical Foundations of Functional Programming, pp. 77\u201386. Addison-Wesley (1994)"},{"key":"23_CR18","unstructured":"Steen, A.: Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master\u2019s thesis, Freie Universit\u00e4t Berlin, Berlin (2014)"},{"issue":"4","key":"23_CR19","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. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"23_CR20","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-20615-8_22","volume-title":"Intelligent Computer Mathematics","author":"M Wisniewski","year":"2015","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: LeoPARD \u2014 A generic platform for the implementation of higher-order reasoners. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 325\u2013330. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:27:54Z","timestamp":1559330874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}