{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:46:04Z","timestamp":1753886764145},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,6,18]],"date-time":"2016-06-18T00:00:00Z","timestamp":1466208000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Deutsche Forschungsgemeinschaft (DFG)","award":["BE 2501\/9-1,2"],"award-info":[{"award-number":["BE 2501\/9-1,2"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Philos Logic"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10992-016-9403-0","type":"journal-article","created":{"date-parts":[[2016,6,18]],"date-time":"2016-06-18T17:43:37Z","timestamp":1466271817000},"page":"333-353","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Cut-Elimination for Quantified Conditional Logic"],"prefix":"10.1007","volume":"46","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,18]]},"reference":[{"key":"9403_CR1","unstructured":"Andrews, P. (2014). Church\u2019s type theory. In Zalta, E.N. (Ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edn.: Stanford University."},{"issue":"3","key":"9403_CR2","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"PB Andrews","year":"1971","unstructured":"Andrews, P.B. (1971). Resolution in type theory. Journal of Symbolic Logic, 36(3), 414\u2013432.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"9403_CR3","doi-asserted-by":"crossref","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B. (1972). General models and extensionality. Journal of Symbolic Logic, 37(2), 395\u2013397.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"9403_CR4","doi-asserted-by":"crossref","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B. (1972). General models, descriptions, and choice in type theory. Journal of Symbolic Logic, 37(2), 385\u2013394.","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"9403_CR5","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s10817-011-9233-2","volume":"47","author":"J Backes","year":"2011","unstructured":"Backes, J., & Brown, C.E. (2011). Analytic tableaux for higher-order logic with choice. Journal of Automated Reasoning, 47(4), 451\u2013479.","journal-title":"Journal of Automated Reasoning"},{"key":"9403_CR6","volume-title":"Equality and extensionality in automated higher-order theorem proving","author":"C Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C. (1999). Equality and extensionality in automated higher-order theorem proving. Ph.D. thesis, Saarland University."},{"key":"9403_CR7","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C. (1999). Extensional higher-order paramodulation and RUE-resolution. In Ganzinger, H. (Ed.) Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, no. 1632 in LNCS, pp. 399\u2013413. : Springer. doi: 10.1007\/3-540-48660-7_39","DOI":"10.1007\/3-540-48660-7_39"},{"key":"9403_CR8","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C. (2009). Automating access control logic in simple type theory with LEO-II. In Gritzalis, D., & L\u00f3pez, J. (Eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009. Proceedings, IFIP, vol. 297, pp. 387\u2013398. doi: 10.1007\/978-3-642-01244-0_34 : Springer.","DOI":"10.1007\/978-3-642-01244-0_34"},{"issue":"1-2","key":"9403_CR9","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s10472-011-9249-7","volume":"62","author":"C Benzm\u00fcller","year":"2011","unstructured":"Benzm\u00fcller, C. (2011). Combining and automating classical and non-classical logics in classical higher-order logic. Annals of Mathematics and Artificial Intelligence (Special issue Computational logics in Multi-agent Systems (CLIMA XI)), 62(1-2), 103\u2013128. doi: 10.1007\/s10472-011-9249-7 .","journal-title":"Annals of Mathematics and Artificial Intelligence (Special issue Computational logics in Multi-agent Systems (CLIMA XI))"},{"key":"9403_CR10","unstructured":"Benzm\u00fcller, C. (2013). Automating quantified conditional logics in HOL. In Rossi, F. (Ed.) 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746-753, Beijing, China."},{"key":"9403_CR11","unstructured":"Benzm\u00fcller, C. (2013). Cut-free calculi for challenge logics in a lazy way. In Clint van Alten Petr Cintula, C.N. (Ed.) Proceedings of the International Workshop on Algebraic Logic in Computer Science."},{"key":"9403_CR12","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C. (2013). A top-down approach to combining logics. In Proc. of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346\u2013351. SciTePress Digital Library, Barcelona, Spain. doi: 10.5220\/0004324803460351 .","DOI":"10.5220\/0004324803460351"},{"key":"9403_CR13","unstructured":"Benzm\u00fcller, C. (2015). Higher-order automated theorem provers. In Delahaye, D., & Woltzenlogel Paleo, B. (Eds.) All about Proofs, Proofs for All, Mathematical Logic and Foundations, pp. 171-214, College Publications."},{"issue":"4","key":"9403_CR14","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., & Kohlhase, M. (2004). Higher-order semantics and extensionality. Journal of Symbolic Logic, 69(4), 1027\u20131088. doi: 10.2178\/jsl\/1102022211 .","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR15","unstructured":"Benzm\u00fcller, C., Brown, C., & Kohlhase, M. (2008). Cut elimination with xi-functionality. In Benzm\u00fcller, C., Brown, c., Siekmann, J., & Statman, R. (Eds.) Reasoning in Simple Type Theory \u2014 Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 84\u2013100. College Publications."},{"issue":"1:6","key":"9403_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-5(1:6)2009","volume":"5","author":"C Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C., Brown, C., & Kohlhase, M. (2009). Cut-simulation and impredicativity. Logical Methods in Computer Science, 5 (1:6), 1\u201321. doi: 10.2168\/LMCS-5(1:6)2009 .","journal-title":"Logical Methods in Computer Science"},{"issue":"1-4","key":"9403_CR17","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10472-012-9320-z","volume":"66","author":"C Benzm\u00fcller","year":"2012","unstructured":"Benzm\u00fcller, C., Gabbay, D., Genovese, V., & Rispoli, D. (2012). Embedding and automating conditional logics in classical higher-order logic. Annals of Mathematics and Artificial Intelligence, 66(1-4), 257\u2013271. doi: 10.1007\/s10472-012-9320-z .","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9403_CR18","unstructured":"Benzm\u00fcller, C., & Genovese, V. Quantified conditional logics are fragments of HOL. In The International Conference on Non-classical Modal and Predicate Logics (NCMPL). Guangzhou (Canton), China (2011). The conference had no published proceedings; the paper is available as. arXiv: 1204.5920v1 ."},{"key":"9403_CR19","unstructured":"Benzm\u00fcller, C., & Paulson, L. (2008). Exploring properties of normal multimodal logics in simple type theory with LEO-II. In Benzm\u00fcller, C., Brown, C., Siekmann, J., & Statman, R. (Eds.) Reasoning in Simple Type Theory \u2014 Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 386\u2013406. College Publications."},{"key":"9403_CR20","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., & Miller, D. (2014). Automation of Higher-Order Logic. Chapter. In Gabbay, D.M., Siekmann, J.H., & Woods, J. (Eds.) Handbook of the History of Logic, Volume 9 \u2014 Computational Logic, North Holland, Elsevier, pp. 215\u2013254.","DOI":"10.1016\/B978-0-444-51624-4.50005-8"},{"issue":"6","key":"9403_CR21","doi-asserted-by":"publisher","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., & Paulson, L. (2010). Multimodal and intuitionistic logics in simple type theory. The Logic Journal of the IGPL, 18(6), 881\u2013892. doi: 10.1093\/jigpal\/jzp080 .","journal-title":"The Logic Journal of the IGPL"},{"issue":"1","key":"9403_CR22","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., & Paulson, L. (2013). Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics), 7(1), 7\u201320. doi: 10.1007\/s11787-012-0052-y .","journal-title":"Logica Universalis (Special Issue on Multimodal Logics)"},{"issue":"4","key":"9403_CR23","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Sultana, N., & Thei\u00df, F. (2015). The higher-order prover LEO-II. Journal of Automated Reasoning, 55(4), 389\u2013404. doi: 10.1007\/s10817-015-9348-y .","journal-title":"Journal of Automated Reasoning"},{"key":"9403_CR24","unstructured":"Benzm\u00fcller, C., & Sultana, N. (2013). LEO-II Version 1.5. In Blanchette , J.C., & Urban, J. (Eds.) PxTP 2013, EPiC Series, vol. 14, pp. 2\u201310. EasyChair."},{"key":"9403_CR25","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., & Woltzenlogel Paleo, B. (2014). Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In Schaub, T., Friedrich, G., & O\u2019Sullivan, B. (Eds.) ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93\u201398. IOS Press. doi: 10.3233\/978-1-61499-419-0-93 .","DOI":"10.3233\/978-1-61499-419-0-93"},{"key":"9403_CR26","unstructured":"Brown, C.E. (2004). Set comprehension in church\u2019s type theory. Ph.D. thesis, Department of Mathematical Sciences Carnegie Mellon University. See also Chad E. Brown (2007), Automated Reasoning in Higher-Order Logic, College Publications."},{"key":"9403_CR27","doi-asserted-by":"crossref","unstructured":"Brown, C.E. (2005). Reasoning in extensional type theory with equality. In Nieuwenhuis, R. (Ed.) Proc. of CADE-20, LNCS, vol. 3632, pp. 23\u201337. Springer.","DOI":"10.1007\/11532231_3"},{"key":"9403_CR28","doi-asserted-by":"publisher","unstructured":"Brown, C.E. (2012). Satallax: An automatic higher-order prover. In Gramlich, B., Miller, D., & Sattler, U. (Eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, LNCS, vol. 7364, pp. 111\u2013117. Springer. doi: 10.1007\/978-3-642-31365-3_11 .","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"9403_CR29","doi-asserted-by":"crossref","unstructured":"Brown, C.E., & Smolka, G. (2010). Analytic tableaux for simple type theory and its first-order fragment. Logical Methods in Computer Science, 6(2).","DOI":"10.2168\/LMCS-6(2:3)2010"},{"issue":"2","key":"9403_CR30","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00693270","volume":"4","author":"B Chellas","year":"1975","unstructured":"Chellas, B. (1975). Basic conditional logic. Journal of Philosophical Logic, 4 (2), 133\u2013153.","journal-title":"Journal of Philosophical Logic"},{"key":"9403_CR31","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal logic: an introduction","author":"B Chellas","year":"1980","unstructured":"Chellas, B. (1980). Modal logic: an introduction. Cambridge: Cambridge University Press."},{"issue":"2","key":"9403_CR32","doi-asserted-by":"crossref","first-page":"346","DOI":"10.2307\/1968337","volume":"33","author":"A Church","year":"1932","unstructured":"Church, A. (1932). A set of postulates for the foundation of logic. Annals of Mathematics, 33(2), 346\u2013366.","journal-title":"Annals of Mathematics"},{"issue":"2","key":"9403_CR33","doi-asserted-by":"crossref","first-page":"354","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A. (1936). An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2), 354\u2013363.","journal-title":"American Journal of Mathematics"},{"issue":"2","key":"9403_CR34","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2), 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR35","volume-title":"The limits of science: Outline of logic and of the methodology of the exact sciences","author":"L Chwistek","year":"1948","unstructured":"Chwistek, L. (1948). The limits of science: Outline of logic and of the methodology of the exact sciences. London: Routledge and Kegan Paul."},{"issue":"1","key":"9403_CR36","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0004-3702(87)90053-1","volume":"33","author":"J Delgrande","year":"1987","unstructured":"Delgrande, J. (1987). A first-order conditional logic for prototypical properties. Artificial Intelligence, 33(1), 105\u2013130.","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"9403_CR37","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0004-3702(98)00088-5","volume":"105","author":"J Delgrande","year":"1998","unstructured":"Delgrande, J. (1998). On first-order conditional logics. Artificial Intelligence, 105(1\u20132), 105\u2013137.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"9403_CR38","doi-asserted-by":"crossref","first-page":"621","DOI":"10.2178\/jsl\/1190150101","volume":"67","author":"M Fitting","year":"2002","unstructured":"Fitting, M. (2002). Interpolation for first order S5. Journal of Symbolic Logic, 67(2), 621\u2013634.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR39","unstructured":"Frege, G. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879). Translated in [43]."},{"issue":"2","key":"9403_CR40","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/359496.359500","volume":"1","author":"N Friedman","year":"2000","unstructured":"Friedman, N., Halpern, J., & Koller, D. (2000). First-order conditional logic for default reasoning revisited. ACM Transactions on Computational Logic, 1(2), 175\u2013207.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9403_CR41","doi-asserted-by":"crossref","unstructured":"Girard, J.Y. (1971). Une extension de l\u2019interpretation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types. In Fenstad, J.E. (Ed.) 2nd scandinavian logic symposium, pp. 63\u201392, North-Holland, Amsterdam.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"9403_CR42","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K. (1931). \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik, 38, 173\u2013198.","journal-title":"Monatshefte der Mathematischen Physik"},{"key":"9403_CR43","unstructured":"van Heijenoort, J. (1967). From Frege to G\u00f6del: A source Book in Mathematics, 1879\u20131931, 3rd printing, 1997 edn. Source books in the history of the sciences series. Harvard University Press, Cambridge, MA."},{"issue":"2","key":"9403_CR44","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L. (1950). Completeness in the theory of types. Journal of Symbolic Logic, 15(2), 81\u201391.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR45","unstructured":"Huet, G.P. (1972). Constrained resolution: a complete method for higher order logic. Ph.D. thesis, Case Western Reserve University."},{"key":"9403_CR46","unstructured":"Huet, G.P. (1973). A mechanization of type theory. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139\u2013146."},{"key":"9403_CR47","volume-title":"A mechanization of sorted higher-order logic based on the resolution principle","author":"M Kohlhase","year":"1994","unstructured":"Kohlhase, M. (1994). A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. thesis, Saarland University."},{"issue":"1","key":"9403_CR48","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R McDowell","year":"2002","unstructured":"McDowell, R., & Miller, D. (2002). Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1), 80\u2013136.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"9403_CR49","doi-asserted-by":"crossref","first-page":"479","DOI":"10.2307\/2586480","volume":"64","author":"G Mints","year":"1999","unstructured":"Mints, G. (1999). Cut-elimination for simple type theory with an axiom of choice. Journal of Symbolic Logic, 64(2), 479\u2013485.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"9403_CR50","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2178\/jsl\/1174668386","volume":"72","author":"R Muskens","year":"2007","unstructured":"Muskens, R. (2007). Intensional models for the theory of types. Journal of Symbolic Logic, 72(1), 98\u2013118.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR51","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-8966-5","volume-title":"Topics in conditional logic","author":"D Nute","year":"1980","unstructured":"Nute, D. (1980). Topics in conditional logic. Dordrecht: Reidel."},{"key":"9403_CR52","doi-asserted-by":"crossref","unstructured":"Olivetti, N., Pozzato, G., & Schwind, C. (2007). A sequent calculus and a theorem prover for standard conditional logics. ACM Transactions on Computational Logic, 8(4).","DOI":"10.1145\/1276920.1276924"},{"key":"9403_CR53","unstructured":"Paleo, B.W. (2014). An embedding of neighbourhood-based modal logics in hol. Unpublished draft; available at https:\/\/github.com\/Paradoxika\/ModalLogic ."},{"key":"9403_CR54","doi-asserted-by":"publisher","unstructured":"Pattinson, D., & Schr\u00f6der, L. (2011). Generic modal cut elimination applied to conditional logics. Logical Methods in Computer Science, 7(1). doi: 10.2168\/LMCS-7(1:4)2011 .","DOI":"10.2168\/LMCS-7(1:4)2011"},{"issue":"3","key":"9403_CR55","doi-asserted-by":"crossref","first-page":"452","DOI":"10.2307\/2270331","volume":"33","author":"D Prawitz","year":"1968","unstructured":"Prawitz, D. (1968). Hauptsatz for higher order logic. Journal of Symbolic Logic, 33(3), 452\u2013457.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR56","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P. (1926). The foundations of mathematics. In Proceedings of the London Mathematical Society, 2, vol. 25, pp. 338\u2013384.","DOI":"10.1112\/plms\/s2-25.1.338"},{"issue":"1\u20133","key":"9403_CR57","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.apal.2007.08.001","volume":"149","author":"J Rasga","year":"2007","unstructured":"Rasga, J. (2007). Sufficient conditions for cut elimination with complexity analysis. Annals of Pure and Applied Logic, 149(1\u20133), 81\u201399. doi: 10.1016\/j.apal.2007.08.001 .","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"9403_CR58","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B Russell","year":"1908","unstructured":"Russell, B. (1908). Mathematical logic as based on the theory of types. American Journal of Mathematics, 30(3), 222\u2013262.","journal-title":"American Journal of Mathematics"},{"issue":"4","key":"9403_CR59","doi-asserted-by":"crossref","first-page":"305","DOI":"10.2307\/2963525","volume":"25","author":"K Sch\u00fctte","year":"1960","unstructured":"Sch\u00fctte, K. (1960). Semantical and syntactical properties of simple type theory. Journal of Symbolic Logic, 25(4), 305\u2013326.","journal-title":"Journal of Symbolic Logic"},{"key":"9403_CR60","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1073\/pnas.49.6.828","volume":"49","author":"RM Smullyan","year":"1963","unstructured":"Smullyan, R.M. (1963). A unifying principle for quantification theory. Proc Nat Acad Sciences, 49, 828\u2013832.","journal-title":"Proc Nat Acad Sciences"},{"key":"9403_CR61","doi-asserted-by":"crossref","unstructured":"Stalnaker, R. (1968). A theory of conditionals. In Studies in Logical Theory , pp. 98\u2013112. Blackwell.","DOI":"10.1007\/978-94-009-9117-0_2"},{"issue":"4","key":"9403_CR62","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G. (2009). The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4), 337\u2013362.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"9403_CR63","first-page":"1","volume":"73","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., & Benzm\u00fcller, C. (2010). Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, 73(1), 1\u201327.","journal-title":"Journal of Formalized Reasoning"},{"issue":"6","key":"9403_CR64","doi-asserted-by":"crossref","first-page":"980","DOI":"10.1090\/S0002-9904-1966-11611-7","volume":"72","author":"WW Tait","year":"1966","unstructured":"Tait, W.W. (1966). A nonconstructive proof of Gentzen\u2019s Hauptsatz for second order predicate logic. Bulletin of the American Mathematical Society, 72(6), 980\u2013983.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"9403_CR65","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","volume":"19","author":"M Takahashi","year":"1967","unstructured":"Takahashi, M. (1967). A proof of cut-elimination theorem in simple type theory. Journal of the Mathematical Society of Japan, 19, 399\u2013410.","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"9403_CR66","first-page":"149","volume":"24","author":"G Takeuti","year":"1954","unstructured":"Takeuti, G. (1954). On a generalized logic calculus. Japanese. Journal of Mathematics 23, 39\u201396 (1953). Errata: ibid, 24, 149\u2013156.","journal-title":"Journal of Mathematics 23, 39\u201396 (1953). Errata: ibid"},{"key":"9403_CR67","doi-asserted-by":"crossref","first-page":"238","DOI":"10.2969\/jmsj\/01230238","volume":"12","author":"G Takeuti","year":"1960","unstructured":"Takeuti, G. (1960). An example on the fundamental conjecture of GLC. Journal of the Mathematical Society of Japan, 12, 238\u2013242.","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"9403_CR68","unstructured":"Takeuti, G. (1975). Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 81. Elsevier."},{"key":"9403_CR69","unstructured":"Wisniewski, M., & Steen, A. (2015). Embedding of First-Order Nominal Logic into Higher-Order Logic. In Beziau, J. Y. et al. Handbook of the 5th world congress and school on universal logic (UNILOG\u201915), Istanbul, Turkey (pp. 337\u2013339)."}],"container-title":["Journal of Philosophical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-016-9403-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10992-016-9403-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-016-9403-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10992-016-9403-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T22:59:07Z","timestamp":1568069947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10992-016-9403-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,18]]},"references-count":69,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9403"],"URL":"https:\/\/doi.org\/10.1007\/s10992-016-9403-0","relation":{},"ISSN":["0022-3611","1573-0433"],"issn-type":[{"value":"0022-3611","type":"print"},{"value":"1573-0433","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,18]]}}}