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.


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.


BSD License


Session AnselmGod