Reference : Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Arts & humanities : Philosophy & ethics
Arts & humanities : Religion & theology
Computational Sciences
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Fuenmayor, David []
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI
Springer International Publishing AG
40th Annual German Conference on AI
from 25-09-2017 to 29-09-2017
[en] Ontological Argument ; Intensional Higher-Order Modal Logic ; Formal Methods ; Automated Reasoning
[en] A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work.
Researchers ; Professionals ; Students

File(s) associated to this reference

Fulltext file(s):

Open access
C65.pdfAuthor preprint481.96 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.