GoedelGod

Gödel’s God in Isabelle/HOL. Dana Scott’s version of Gödel’s proof of God’s existence is formalized in quantified modal logic KB (QML KB). QML KB is modeled as a fragment of classical higher-order logic (HOL); thus, the formalization is essentially a formalization in HOL.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 7 articles , 1 standard article )

Showing results 1 to 7 of 7.
Sorted by year (citations)

  1. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  2. Woltzenlogel Paleo, Bruno: Para-disagreement logics and their implementation through embedding in Coq and SMT (2018)
  3. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  4. Benzmüller, Christoph: Higher-order automated theorem provers (2015)
  5. Benzmüller, Christoph: Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics (2015)
  6. Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: Interacting with modal logics in the Coq proof assistant (2015)
  7. Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: On logic embeddings and Gödel’s God (2015)