Formalization, Mechanization and Automation of G\"odel's Proof of God's Existence
From MaRDI portal
Publication:6244239
DOI10.3233/978-1-61499-419-0-93arXiv1308.4526MaRDI QIDQ6244239FDOQ6244239
Authors: Christoph Benzmüller, Bruno Woltzenlogel Paleo 
Publication date: 21 August 2013
Abstract: G"odel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis.
Knowledge representation (68T30) Logic in artificial intelligence (68T27) Philosophical aspects of logic and foundations (03Axx)
This page was built for publication: Formalization, Mechanization and Automation of G\"odel's Proof of God's Existence
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6244239)
