{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T04:16:05Z","timestamp":1750997765334,"version":"3.41.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_2","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T15:43:26Z","timestamp":1510328606000},"page":"7-11","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"key":"2_CR1","unstructured":"Bentert, M., Benzm\u00fcller, C., Streit, D., Woltzenlogel Paleo, B.: Analysis of an ontological proof proposed by Leibniz. In: Tandy, C. (ed.) Death and Anti-Death. Four Decades after Michael Polanyi, Three Centuries after G.W. Leibniz, vol. 14. Ria University Press (2016)"},{"key":"2_CR2","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-01244-0_34","volume-title":"Emerging Challenges for Security, Privacy and Trust","author":"C Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C.: Automating access control logics in simple type theory with LEO-II. In: Gritzalis, D., Lopez, J. (eds.) SEC 2009. IAICT, vol. 297, pp. 387\u2013398. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01244-0_34"},{"issue":"1\u20132","key":"2_CR3","first-page":"103","volume":"62","author":"C Benzm\u00fcller","year":"2011","unstructured":"Benzm\u00fcller, C.: Combining and automating classical and non-classical logics in classical higher-order logic. Ann. Math. Artif. Intell. (Special Issue Computational logics in Multi-agent Systems (CLIMA XI)) 62(1\u20132), 103\u2013128 (2011)","journal-title":"Ann. Math. Artif. Intell. (Special Issue Computational logics in Multi-agent Systems (CLIMA XI))"},{"key":"2_CR4","unstructured":"Benzm\u00fcller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) IJCAI 2013, pp. 746\u2013753. AAAI Press (2013)"},{"issue":"3","key":"2_CR5","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","volume":"46","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333\u2013353 (2017)","journal-title":"J. Philos. Logic"},{"key":"2_CR6","series-title":"Computational Logic","first-page":"215","volume-title":"Handbook of the History of Logic","author":"C Benzm\u00fcller","year":"2014","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic. Computational Logic, vol. 9, pp. 215\u2013254. North Holland, Elsevier (2014)"},{"issue":"6","key":"2_CR7","doi-asserted-by":"crossref","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Paulson, L.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881\u2013892 (2010)","journal-title":"Logic J. IGPL"},{"issue":"1","key":"2_CR8","first-page":"7","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univ. (Special Issue on Multimodal Logics) 7(1), 7\u201320 (2013)","journal-title":"Logica Univ. (Special Issue on Multimodal Logics)"},{"issue":"4","key":"2_CR9","doi-asserted-by":"crossref","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.: The higher-order prover LEO-II. J. Autom. Reasoning 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-42432-3_6","volume-title":"Mathematical Software \u2013 ICMS 2016","author":"C Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C., Scott, D.: Automating Free Logic in Isabelle\/HOL. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 43\u201350. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42432-3_6"},{"key":"2_CR11","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Axiomatizing category theory in free logic (2016). arXiv, http:\/\/arxiv.org\/abs\/1609.01493"},{"issue":"1","key":"2_CR12","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/s11787-017-0160-9","volume":"11","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-H\u00e1jek controversy. Logica Univ. 11(1), 139\u2013151 (2017)","journal-title":"Logica Univ."},{"key":"2_CR13","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: G\u00f6del\u2019s God in Isabelle\/HOL. Archive of Formal Proofs (2013). (Formally verified)"},{"key":"2_CR14","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: 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 (2014)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-319-20297-6_25","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Interacting with modal logics in the coq proof assistant. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 398\u2013411. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20297-6_25"},{"key":"2_CR16","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: The inconsistency in G\u00f6del\u2019s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016. vol. 1\u20133, pp. 936\u2013942. AAAI Press (2016)"},{"key":"2_CR17","series-title":"Studies in Universal Logic","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-45062-9_18","volume-title":"The Square of Opposition: A Cornerstone of Thought","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C., Paleo, B.W.: The ontological modal collapse as a collapse of the square of opposition. In: B\u00e9ziau, J.-Y., Basti, G. (eds.) The Square of Opposition: A Cornerstone of Thought. SUL, pp. 307\u2013313. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-45062-9_18"},{"key":"2_CR18","first-page":"43","volume":"9","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Experiments in Computational Metaphysics: G\u00f6del\u2019s proof of God\u2019s existence. Savijnanam: scientific exploration for a spiritual paradigm. J. Bhaktivedanta Inst. 9, 43\u201357 (2017)","journal-title":"J. Bhaktivedanta Inst."},{"key":"2_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"2_CR20","volume-title":"The Logic of Provability","author":"G Boolos","year":"1993","unstructured":"Boolos, G.: The Logic of Provability. Cambridge University Press, Cambridge (1993)"},{"key":"2_CR21","doi-asserted-by":"crossref","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. Symbolic Logic 5, 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"2_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-0411-4","volume-title":"Types, Tableaus, and G\u00f6del\u2019s God","author":"M Fitting","year":"2002","unstructured":"Fitting, M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer, Amsterdam (2002)"},{"key":"2_CR23","volume-title":"Categories","author":"PJ Freyd","year":"1990","unstructured":"Freyd, P.J., Scedrov, A.: Categories. North Holland, Allegories (1990)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-67190-1_9","volume-title":"Advances in Artificial Intelligence","author":"D Fuenmayor","year":"2017","unstructured":"Fuenmayor, D., Benzm\u00fcller, C.: Automating emendations of the ontological argument in intensional higher-order modal logic. In: Kern-Isberner, G., F\u00fcrnkranz, J., Thimm, M. (eds.) KI 2017. Lecture Notes in Computer Science, vol. 10505, pp. 114\u2013127. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67190-1_9"},{"key":"2_CR25","unstructured":"G\u00f6del, K.: Appx. A: Notes in Kurt G\u00f6del\u2019s Hand. In: Sobel [33], pp. 144\u2013145 (1970)"},{"key":"2_CR26","unstructured":"Kirchner, D.: Representation and partial automation of the principia logico-metaphysica in Isabelle\/HOL. Archive of Formal Proofs (2017). formally verified with Isabelle\/HOL"},{"key":"2_CR27","unstructured":"Lachnitt, H.: Systematic verification of the intuitionistic modal logic cube in isabelle\/hol. Bachelor Thesis at the Freie Universit\u00e4t Berlin, Institut f\u00fcr Informatik (2017)"},{"key":"2_CR28","volume-title":"Free Logic. Selected Essays","author":"K Lambert","year":"2012","unstructured":"Lambert, K.: Free Logic. Selected Essays. Cambridge University Press, Cambridge (2012)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"2","key":"2_CR30","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1093\/logcom\/exq017","volume":"21","author":"PE Oppenheimer","year":"2011","unstructured":"Oppenheimer, P.E., Zalta, E.N.: Relations versus functions at the foundations of logic: type-theoretic considerations. J. Log. Comput. 21(2), 351\u2013374 (2011)","journal-title":"J. Log. Comput."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Scott, D.: Appx. B: Notes in Dana Scott\u2019s Hand. In: Sobel [33], pp. 145\u2013146 (1972)","DOI":"10.1016\/0020-1383(72)90052-6"},{"key":"2_CR32","first-page":"181","volume-title":"Bertrand Russell: Philosopher of the Century","author":"D Scott","year":"1967","unstructured":"Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181\u2013200. George Allen & Unwin, London (1967). (Reprinted with additions. In: Philosophical Application of Free Logic, edited by K. Lambert. Oxford Universitry Press, 1991, pp. 28\u201348)"},{"key":"2_CR33","volume-title":"Logic and Theism","author":"J Sobel","year":"2004","unstructured":"Sobel, J.: Logic and Theism. Cambridge U. Press, Cambridge (2004)"},{"key":"2_CR34","doi-asserted-by":"crossref","first-page":"535","DOI":"10.12775\/LLP.2016.021","volume":"25","author":"A Steen","year":"2016","unstructured":"Steen, A., Benzm\u00fcller, C.: Sweet SIXTEEN: automation via embedding into classical higher-order logic. Logic Logical Philos. 25, 535\u2013554 (2016)","journal-title":"Logic Logical Philos."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Steen, A., Wisniewski, M., Benzm\u00fcller, C.: Tutorial on reasoning in expressive non-classical logics with Isabelle\/HOL. In: Benz\u00fcller, C., Rojas, R., Sutcliffe, G. (eds.) GCAI 2016. EPiC Series in Computing, vol. 41, pp. 1\u201310. EasyChair (2016)","DOI":"10.29007\/4dsr"},{"key":"2_CR36","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: Einsatz von Theorembeweisern in der Lehre. In: Schwill, A., Lucke, U. (eds.) Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung\/Didaktik der Informatik. Commentarii informaticae didacticae (CID), Universit\u00e4tsverlag Potsdam, Potsdam, Germany (2016)"},{"key":"2_CR37","unstructured":"Zalta, E.N.: Principia logico-metaphysica (2016). draft version, preprint https:\/\/mally.stanford.edu\/principia.pdf"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T23:54:39Z","timestamp":1750982079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}