The Ontological Argument in PVS

John Rushby

Invited paper presented at the CAV Workshop Fun With Formal Methods, St. Petersburg, Russia, 13 July 2013.

Abstract

The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in PVS and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.

PDF

Slides

PDF

PVS files

ontological.dmp

BibTeX Entry

@INPROCEEDINGS{Rushby13:ontological,
	AUTHOR = {John Rushby},
	TITLE = {The {Ontological Argument} in {PVS}},
	BOOKTITLE = {Fun With Formal Methods},
	YEAR = 2013,
	EDITOR = {Nikolay Shilov},
	ADDRESS = {St~Petersburg, Russia},
	MONTH = jul,
	NOTE = {Workshop in association with CAV'13}
}

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