Reference : Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science Arts & humanities : Philosophy & ethics Arts & humanities : Religion & theology
	Focus Areas :	Computational Sciences
	To cite this reference:	http://hdl.handle.net/10993/33693

Title :	Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Language :	English
Author, co-author :	Fuenmayor, David []
	Benzmüller, Christoph [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Publication date :	Sep-2017
Main document title :	KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI
Publisher :	Springer International Publishing AG
Peer reviewed :	Yes
On invitation :	No
Audience :	International
ISBN :	978-3-319-67189-5
City :	Cham
Country :	Switzerland
Event name :	40th Annual German Conference on AI
Event date :	from 25-09-2017 to 29-09-2017
Keywords :	[en] Ontological Argument ; Intensional Higher-Order Modal Logic ; Formal Methods ; Automated Reasoning
Abstract :	[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.
Target :	Researchers ; Professionals ; Students
Permalink :	http://hdl.handle.net/10993/33693
DOI :	10.1007/978-3-319-67190-1_9
Other URL :	http://christoph-benzmueller.de/papers/C65.pdf

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Open access C65.pdf Author preprint 481.96 kB View/Open

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map