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

John Rushby

CSL Technical Note, January 2016 *NEW* This technnical note is largely subsumed by a later journal paper

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