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.
I have several more recent papers on the
Ontological Argument.
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