{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T14:26:33Z","timestamp":1766759193505},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T00:00:00Z","timestamp":1487808000000},"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":["Log. Univers."],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s11787-017-0160-9","type":"journal-article","created":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T15:29:20Z","timestamp":1487863760000},"page":"139-151","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Computer-Assisted Analysis of the Anderson\u2013H\u00e1jek Ontological Controversy"],"prefix":"10.1007","volume":"11","author":[{"given":"C.","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"L.","family":"Weber","sequence":"additional","affiliation":[]},{"given":"B.","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,23]]},"reference":[{"key":"160_CR1","unstructured":"Rushby, J.: The ontological argument in PVS. In: Proceedings of CAV Workshop \u201cFun With Formal Methods\u201d. St. Petersburg, Russia (2013)"},{"issue":"2","key":"160_CR2","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1080\/00048401003674482","volume":"89","author":"PE Oppenheimer","year":"2011","unstructured":"Oppenheimer, 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":"160_CR3","first-page":"144","volume-title":"Logic and Theism: Arguments for and Against Beliefs in God","author":"K G\u00f6del","year":"2004","unstructured":"G\u00f6del, K.: Appx.A: notes in Kurt G\u00f6del\u2019s hand. In: Sobel, J.H. (ed.) Logic and Theism: Arguments for and Against Beliefs in God, pp. 144\u2013145. Cambridge University Press, Cambridge (2004)"},{"key":"160_CR4","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-942. AAAI Press (2016). URL: http:\/\/www.ijcai.org\/Proceedings\/16\/Papers\/137.pdf"},{"key":"160_CR5","doi-asserted-by":"publisher","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, vol. 263. Frontiers in Artificial Intelligence and Applications, pp. 93\u201398. IOS Press, Amsterdam (2014). doi: 10.3233\/978-1-61499-419-0-93","DOI":"10.3233\/978-1-61499-419-0-93"},{"key":"160_CR6","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of G\u00f6del\u2019s Proof of God\u2019s Existence. arXiv:1308.4526"},{"key":"160_CR7","doi-asserted-by":"publisher","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Sultana, N., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015). doi: 10.1007\/s10817-015-9348-y","DOI":"10.1007\/s10817-015-9348-y"},{"key":"160_CR8","first-page":"145","volume-title":"Logic and Theism: Arguments for and Against Beliefs in God","author":"D Scott","year":"2004","unstructured":"Scott, D.: Appx.B: notes in Dana Scott\u2019s hand. In: Sobel, J.H. (ed.) Logic and Theism: Arguments for and Against Beliefs in God, pp. 145\u2013146. Cambridge University Press, Cambridge (2004)"},{"key":"160_CR9","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":"160_CR10","unstructured":"Sobel, J.H.: G\u00f6del\u2019s ontological proof. In: On Being and Saying. Thomson, JJ. (ed.) Essays for Richard Cartwright, pp. 241\u2013261. MIT Press, Cambridge, Mass (1987)"},{"key":"160_CR11","unstructured":"Hajek, P.: Der Mathematiker und die Frage der Existenz Gottes. In: Buldt, B., K\u00f6hler, E., St\u00f6ltzner, M., Weibel P., Klein, C., Depauli-Schimanowich-G\u00f6ttig, W. (eds.) Kurt G\u00f6del. Wahrheit und Beweisbarkeit. ISBN 3-209-03835-X. \u00f6bv & hpt, Wien, pp. 325\u2013336 (2001)"},{"key":"160_CR12","doi-asserted-by":"crossref","unstructured":"Hajek, P.: Magari and others on G\u00f6del\u2019s ontological proof. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra, pp. 125\u2013135. Dekker, New York (1996)","DOI":"10.1201\/9780203748671-5"},{"key":"160_CR13","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)"},{"issue":"3","key":"160_CR14","doi-asserted-by":"crossref","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."},{"issue":"2","key":"160_CR15","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. Log. 71(2), 149\u2013164 (2002). doi: 10.1023\/A:1016583920890","journal-title":"Stud. Log."},{"key":"160_CR16","unstructured":"Bj\u00f8rdal, F.: Understanding G\u00f6del\u2019s ontological argument. In: Childers, T. (ed.) The Logica Yearbook 1998. Institute of Philosophy of the Academy of Sciences of the Czech Republic, Filosofia (1999)"},{"issue":"1","key":"160_CR17","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.C.: Quantified multimodal logics in simple type theory. Log. Univers. 7(1), 7\u201320 (2013). doi: 10.1007\/s11787-012-0052-y","journal-title":"Log. Univers."},{"key":"160_CR18","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"160_CR19","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: an automated higher-order prover. In: Proceedings of lJCAR 2012. LNAI 7364, pp. 111\u2013117. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"160_CR20","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-Level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10\u201313, 2007, Proceedings, vol. 4732. Lecture Notes in Computer Science. Springer, pp. 232\u2013245 (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"160_CR21","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies\/Tactics in Higher Order Logics, NASA Tech. Rep. NASA\/CP-2003-212448, pp. 56\u201368 (2003)"},{"key":"160_CR22","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Proceedings of lTP 2010. LNCS 6172, pp. 131\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"160_CR23","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson\u2013Hajek ontological controversy (presentation abstract). In: Silvestre, R.S., Beziau, J.-Y. (eds.) Handbook of the 1st World Congress on Logic and Religion, pp. 53\u201354. Joao Pessoa, Brasil (2015)"},{"issue":"4","key":"160_CR24","first-page":"11","volume":"7","author":"R Magari","year":"1988","unstructured":"Magari, R.: Logica e Teofilia. Notizie di Logica 7(4), 11\u201320 (1988)","journal-title":"Notizie di Logica"},{"key":"160_CR25","doi-asserted-by":"crossref","unstructured":"Anderson, A.C., Gettings, M.: G\u00f6del ontological proof revisited. In: G\u00f6del\u201996: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6, pp. 167\u2013172. Springer (1996)","DOI":"10.1017\/9781316716939.011"},{"key":"160_CR26","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1111\/j.1755-2567.1969.tb00361.x","volume":"35","author":"NB Cocchiarella","year":"1969","unstructured":"Cocchiarella, N.B.: A completeness theorem in second order modal logic. Theoria 35, 81\u2013103 (1969)","journal-title":"Theoria"}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-017-0160-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-017-0160-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-017-0160-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T00:57:14Z","timestamp":1568854634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-017-0160-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,23]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["160"],"URL":"https:\/\/doi.org\/10.1007\/s11787-017-0160-9","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,23]]}}}