Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Anselm's God in Isabelle/HOL

view this post on Zulip Email Gateway (Aug 22 2022 at 16:04):

From: Lawrence Paulson <lp15@cam.ac.uk>
We now have another proof of the existence of God along with another formalisation of free logic, thanks to Ben Blumson:

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.

You will find it online here: https://www.isa-afp.org/entries/AnselmGod.html

Still waiting for proofs of the existence of Satan.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 16:05):

From: Julian Parsert <parsert.julian@gmail.com>
It seems like the references in the proof document are not working as
intended.

https://www.isa-afp.org/browser_info/current/AFP/AnselmGod/document.pdf

Julian Parsert

Last updated: May 06 2024 at 08:19 UTC