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
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
- Woltzenlogel Paleo, Bruno: Para-disagreement logics and their implementation through embedding in Coq and SMT (2018)
- Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
- Benzmüller, Christoph: Higher-order automated theorem provers (2015)
- Benzmüller, Christoph: Invited talk: on a (quite) universal theorem proving approach and its application in metaphysics (2015)
- Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: Interacting with modal logics in the coq proof assistant (2015)
- Benzmüller, Christoph; Paleo, Bruno Woltzenlogel: On logic embeddings and Gödel’s god (2015)