Anselm's God in Isabelle/HOL

Ben Blumson 🌐

September 6, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Paul Oppenheimer and Edward Zalta's formalisation of Anselm's ontological argument for the existence of God is automated by embedding a free logic for definite descriptions within Isabelle/HOL.

License

BSD License

Topics

Session AnselmGod

Cite

× 
@article{AnselmGod-AFP,
  author  = {Ben Blumson},
  title   = {Anselm's God in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/AnselmGod.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: