Mechanized Analysis of a Formalization of Anselm's Ontological Argument by Eder and Ramharter

John Rushby

CSL Technical Note, January 2016

Abstract

Eder and Ramharter propose requirements to be satisfied by formal reconstructions of informal arguments and illustrate these with their own reconstructions of Anselm's Ontological Argument: one in classical (higher-order) logic, and one in modal logic. I reproduce and mechanically check their classical reconstruction in the PVS verification system and present this as an illustration of the ease and benefit of mechanized analysis in this domain. I hope this may stimulate philosophers and theologians to investigate these tools from computer science, and to explore their application to topics of philosophical interest.

PDF

Slides

PDF

BibTeX Entry

@TECHREPORT{Rushby:ER-OntArg16,
	AUTHOR = {John Rushby},
	TITLE = {Mechanized Analysis of a Formalization of Anselm's
                 Ontological Argument by Eder and Ramharter},
        TYPE = {CSL Technical Note},
	INSTITUTION = {Computer Science Laboratory, SRI International},
	YEAR = 2016,
	ADDRESS = {Menlo Park, CA},
	MONTH = jan
}


Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page