On logic embeddings and Gödel’s god. (English) Zbl 06545645

Benzmüller, Christoph; Paleo, Bruno Woltzenlogel

Codescu, Mihai (ed.) et al., Recent trends in algebraic development techniques. 22nd international workshop, WADT 2014, Sinaia, Romania, September 4–7, 2014. Revised selected papers. Cham: Springer (ISBN 978-3-319-28113-1/pbk; 978-3-319-28114-8/ebook). Lecture Notes in Computer Science 9463, 3-6 (2015).

Summary: We have applied an elegant and flexible logic embedding approach to verify and automate a prominent philosophical argument: the ontological argument for the existence of God. In our ongoing computer-assisted study, higher-order automated reasoning tools have made some interesting observations, some of which were previously unknown.
For the entire collection see [Zbl 1327.68013].

MSC:

68Qxx

Theory of computing

Software:

GoedelGod; Isabelle/HOL; LEO-II; Nitpick; PVS; Satallax; TPTP