{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:10:02Z","timestamp":1748736602434,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319281131"},{"type":"electronic","value":"9783319281148"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-28114-8_1","type":"book-chapter","created":{"date-parts":[[2015,12,29]],"date-time":"2015-12-29T12:57:37Z","timestamp":1451393857000},"page":"3-6","source":"Crossref","is-referenced-by-count":1,"title":["On Logic Embeddings and G\u00f6del\u2019s God"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Bruno Woltzenlogel","family":"Paleo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,30]]},"reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"291","DOI":"10.5840\/faithphil19907325","volume":"7","author":"CA Anderson","year":"1990","unstructured":"Anderson, C.A.: Some emendations of G\u00f6del\u2019s ontological proof. Faith Philos. 7(3), 291\u2013303 (1990)","journal-title":"Faith Philos."},{"key":"1_CR2","unstructured":"Anderson, C.A., Gettings, M.: G\u00f6del ontological proof revisited. In: G\u00f6del\u201996: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6, pages 167\u2013172. Springer, (1996)"},{"key":"1_CR3","unstructured":"Benzm\u00fcller, C.: Automating quantified conditional logics in HOL. In: Proceedings of IJCAI 2013, pp. 746\u2013753, Beijing, China (2013)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: A top-down approach to combining logics. In: Proceedings of ICAART 2013, pp. 346\u2013351. SciTePress Digital Library, Barcelona, Spain (2013)","DOI":"10.5220\/0004324803460351"},{"key":"1_CR5","unstructured":"Benzm\u00fcller, C., Paleo, B.W.: G\u00f6del\u2019s God in Isabelle\/HOL. Arch. Formal Proofs (2013)"},{"key":"1_CR6","unstructured":"Benzm\u00fcller, C., Paleo, B.W.: Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In: ECAI 2014. Frontiers in AI and Applications, vol. 263, pp. 163\u2013168. IOS Press (2014)"},{"key":"1_CR7","unstructured":"Benzm\u00fcller, C., Weber, L., Paleo, B.W.: Computer-assisted analysis of the Anderson-H\u00e1jek ontological controversy. Handbook of the 1st World Congress on Logic and Religion, Jo\u00e3o Pessoa, Brazil (2015)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. (ed.) CSR 2015. LNCS, vol. 9139, pp. 398\u2013411. Springer, Heidelberg (2015)"},{"issue":"1","key":"1_CR9","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.: Quantified multimodal logics in simple type theory. Logica Univers. (Spec. Issue Multimodal Logics) 7(1), 7\u201320 (2013)","journal-title":"Logica Univers. (Spec. Issue Multimodal Logics)"},{"key":"1_CR10","series-title":"lecture notes in computer science (lecture notes in artificial intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"CE Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"1_CR11","unstructured":"Bj\u00f8rdal, F.: Understanding G\u00f6del\u2019s ontological argument. In: The Logica Yearbook 1998. Filosofia (1999)"},{"key":"1_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)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"1_CR14","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. Symbolic Logic 5, 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"1_CR15","series-title":"Synthese Library","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic","author":"M Fitting","year":"1998","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Synthese Library, vol. 277. Kluwer, Dordrecht (1998)"},{"key":"1_CR16","doi-asserted-by":"publisher","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, Norwell (2002)"},{"key":"1_CR17","unstructured":"Fuhrmann, A.: Existenz und Notwendigkeit \u2013 Kurt G\u00f6dels axiomatische Theologie. In: Logik in der Philosophie, Heidelberg (Synchron) (2005)"},{"key":"1_CR18","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"DM Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996)"},{"key":"1_CR19","unstructured":"G\u00f6del, K.: Appx.A: notes in Kurt G\u00f6del\u2019s hand. In: [25], pp. 144\u2013145 (2004)"},{"issue":"2","key":"1_CR20","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1016583920890","volume":"71","author":"P Hajek","year":"2002","unstructured":"Hajek, P.: A new small emendation of G\u00f6del\u2019s ontological proof. Stud. Logica: Int. J. Symbolic Logic 71(2), 149\u2013164 (2002)","journal-title":"Stud. Logica: Int. J. Symbolic Logic"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s11225-008-9151-4","volume":"90","author":"P Hajek","year":"2008","unstructured":"Hajek, P.: Ontological proofs of existence and non-existence. Stud. Logica: Int. J. Symbolic Logic 90(2), 257\u2013262 (2008)","journal-title":"Stud. Logica: Int. J. Symbolic Logic"},{"issue":"2","key":"1_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1080\/00048401003674482","volume":"89","author":"PE Oppenheimera","year":"2011","unstructured":"Oppenheimera, P.E., Zalta, E.N.: A computationally-discovered simplification of the ontological argument. Australas. J. Philos. 89(2), 333\u2013349 (2011)","journal-title":"Australas. J. Philos."},{"key":"1_CR23","unstructured":"Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop \u201cFun With Formal Methods\u201d, St. Petersburg, Russia (2013)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Scott, D.: Appx.B: notes in Dana Scott\u2019s hand. In: [25], pp. 145\u2013146 (2004)","DOI":"10.1016\/j.tvjl.2005.04.016"},{"key":"1_CR25","volume-title":"Logic and Theism: Arguments for and Against Beliefs in God","author":"JH Sobel","year":"2004","unstructured":"Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)"},{"key":"1_CR26","first-page":"98","volume-title":"Studies in Logical Theory","author":"RC Stalnaker","year":"1968","unstructured":"Stalnaker, R.C.: A theory of conditionals. In: Rescher, N. (ed.) Studies in Logical Theory, pp. 98\u2013112. Blackwell, Oxford (1968)"},{"issue":"1","key":"1_CR27","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"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28114-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T23:30:43Z","timestamp":1748734243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28114-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319281131","9783319281148"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28114-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}