Benzmuller, ChristophWoltzenlogel Paleo, Bruno2023-02-202150-914xhttp://hdl.handle.net/1885/285349Dana Scott's version [12] (cf. Fig. 1) of G odel's proof of God's existence [8] is formalized in quanti ed modal logic KB (QML KB) within the proof assistant Isabelle/HOL. QML KB is modeled as a fragment of classical higher-order logic (HOL); thus, the formalization is essentially a formalization in HOLapplication/pdfen-AU© 2016 The authors20162021-12-02