Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers

MaRDI QIDQ5282959zbMATH OpenFDO

Authors Christoph Benzmüller, Bruno Woltzenlogel Paleo

Publication date 18 July 2017

Full work available at URL http://ebooks.iospress.nl/volumearticle/36922

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On logic embeddings and Gödel's God
• scientific article; zbMATH DE number 7594144
• Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
• Automating emendations of the ontological argument in intensional higher-order modal logic
• Computer-assisted analysis of the Anderson-Hájek ontological controversy

Cited in

(18)

• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Automated search for Gödel's proofs
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Gödel's second theorem and the provability of God's existence
• Cut-elimination for quantified conditional logic
• Variants of Gödel's ontological proof in a natural deduction calculus
• On logic embeddings and Gödel's God
• Incompleteness, Undecidability and Automated Proofs
• The higher-order prover \textsc{Leo}-II
• Higher-order modal logics: automation and applications
• Para-disagreement logics and their implementation through embedding in Coq and SMT
• Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
• Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
• Computer-assisted analysis of the Anderson-Hájek ontological controversy
• An object-logic explanation for the inconsistency in Gödel's ontological theory
• Gödel's god-like essence
• Notes on Gödel's and Scott's variants of the ontological argument

Describes a project that uses

Uses Software

• LEO-II
• Nitpick
• Isabelle/HOL
• PVS
• TPTP
• Prover9
• Satallax
• E Theorem Prover

This page was built for publication: Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5282959)