{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T14:26:42Z","timestamp":1766759202844,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319671895"},{"type":"electronic","value":"9783319671901"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67190-1_9","type":"book-chapter","created":{"date-parts":[[2017,9,18]],"date-time":"2017-09-18T09:48:49Z","timestamp":1505728129000},"page":"114-127","source":"Crossref","is-referenced-by-count":6,"title":["Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic"],"prefix":"10.1007","author":[{"given":"David","family":"Fuenmayor","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,19]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-21401-6_4","volume-title":"Automated Deduction - CADE-25","author":"J Alama","year":"2015","unstructured":"Alama, J., Oppenheimer, P.E., Zalta, E.N.: Automating Leibniz\u2019s theory of concepts. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 73\u201397. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_4"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, A., Gettings, M.: G\u00f6del ontological proof revisited. In: Hajek, P. (ed.) G\u00f6del 1996: Logical Foundations of Mathematics, Computer Science, and Physics. Lecture Notes in Logic, vol. 6, pp. 167\u2013172. Springer (2001)","DOI":"10.1007\/978-3-662-21963-8_10"},{"issue":"3","key":"9_CR3","doi-asserted-by":"crossref","first-page":"291","DOI":"10.5840\/faithphil19907325","volume":"7","author":"C Anderson","year":"1990","unstructured":"Anderson, C.: Some emendations of G\u00f6del\u2019s ontological proof. Faith Philos. 7(3), 291\u2013303 (1990)","journal-title":"Faith Philos."},{"key":"9_CR4","unstructured":"Benzm\u00fcller, C.: Universal reasoning, rational argumentation and human-machine interaction. arXiv (2017). http:\/\/arxiv.org\/abs\/1703.09620"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Claus, M., Sultana, N.: Systematic verification of the modal logic cube in Isabelle\/HOL. In: Kaliszyk, C., Paskevich, A. (eds.) PxTP 2015, EPTCS, Berlin, Germany, vol. 186, pp. 27\u201341 (2015)","DOI":"10.4204\/EPTCS.186.5"},{"issue":"1","key":"9_CR6","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univers. (Special Issue on Multimodal Logics) 7(1), 7\u201320 (2013)","journal-title":"Logica Univers. (Special Issue on Multimodal Logics)"},{"issue":"1","key":"9_CR7","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 Univers. 11(1), 139\u2013151 (2017)","journal-title":"Logica Univers."},{"key":"9_CR8","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":"9_CR9","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: The inconsistency in G\u00f6del\u2019s ontological argument: a success story for AI in metaphysics. In: IJCAI 2016 (2016)"},{"key":"9_CR10","series-title":"Lecture Notes in Artificial Intelligence","first-page":"205","volume-title":"KI 2016: Advances in Artificial Intelligence","author":"C Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: An object-logic explanation for the inconsistency in G\u00f6del\u2019s ontological theory (extended abstract). In: Helmert, M., Wotawa, F. (eds.) KI 2016: Advances in Artificial Intelligence. LNAI, vol. 9904, pp. 205\u2013244. Springer, Berlin (2016)"},{"key":"9_CR11","unstructured":"Bj\u00f8rdal, F.: Understanding G\u00f6del\u2019s ontological argument. In: Childers, T. (ed.) The Logica Yearbook 1998. Filosofia (1999)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_11"},{"key":"9_CR13","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. Symbol. Logic 5, 56\u201368 (1940)","journal-title":"J. Symbol. Logic"},{"issue":"2","key":"9_CR14","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/s10992-006-9038-7","volume":"36","author":"B Fitelson","year":"2007","unstructured":"Fitelson, B., Zalta, E.N.: Steps toward a computational metaphysics. J. Philos. Logic 36(2), 227\u2013247 (2007)","journal-title":"J. Philos. Logic"},{"key":"9_CR15","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, Dordrecht (2002)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Fitting, M., Mendelsohn, R.: First-Order Modal Logic. Synthese Library, vol. 277. Kluwer, Dordrecht (1998)","DOI":"10.1007\/978-94-011-5292-1"},{"key":"9_CR17","unstructured":"Fuenmayor, D., Benzm\u00fcller, C.: Types, Tableaus and G\u00f6del\u2019s God in Isabelle\/HOL. Archive of Formal Proofs (2017). Formally verified with Isabelle\/HOL"},{"key":"9_CR18","volume-title":"Intensional and Higher-Order Modal Logic","author":"D Gallin","year":"1975","unstructured":"Gallin, D.: Intensional and Higher-Order Modal Logic. N.-Holland, Amsterdam (1975)"},{"key":"9_CR19","unstructured":"G\u00f6del, K.: Appx. A: notes in Kurt G\u00f6del\u2019s hand. In: [27], pp. 144\u2013145 (2004)"},{"issue":"2","key":"9_CR20","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1016583920890","volume":"71","author":"P H\u00e1jek","year":"2002","unstructured":"H\u00e1jek, P.: A new small emendation of G\u00f6del\u2019s ontological proof. Studia Logica 71(2), 149\u2013164 (2002)","journal-title":"Studia Logica"},{"key":"9_CR21","volume-title":"Naming and Necessity","author":"S Kripke","year":"1980","unstructured":"Kripke, S.: Naming and Necessity. Harvard University Press, Cambridge (1980)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"issue":"2","key":"9_CR23","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1080\/00048401003674482","volume":"89","author":"P Oppenheimera","year":"2011","unstructured":"Oppenheimera, P., Zalta, E.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333\u2013349 (2011)","journal-title":"Australas. J. Philos."},{"key":"9_CR24","unstructured":"Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop \u201cFun With Formal Methods\u201d, St. Petersburg, Russia (2013)"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Scott, D.: Appx.B: notes in Dana Scott\u2019s hand. In: [27], pp. 145\u2013146 (2004)","DOI":"10.1016\/j.tvjl.2005.04.016"},{"key":"9_CR26","unstructured":"Sobel, J.: G\u00f6del\u2019s ontological proof. In: On Being and Saying. Essays for Richard Cartwright, pp. 241\u2013261. MIT Press (1987)"},{"key":"9_CR27","volume-title":"Logic and Theism: Arguments for and Against Beliefs in God","author":"J Sobel","year":"2004","unstructured":"Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge U. Press, Cambridge (2004)"},{"key":"9_CR28","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, 13\u201314 September 2016 an der Universit\u00e4t Potsdam, Commentarii informaticae didacticae (CID), Potsdam, Germany (2016)"}],"container-title":["Lecture Notes in Computer Science","KI 2017: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67190-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T19:49:32Z","timestamp":1750880972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67190-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319671895","9783319671901"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67190-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}