 The above technique can be exploited for a natural encoding and automated assessment of Gödel’s ontological argument in higher-order modal logic, which unfolds into formulas in Church’s type theory such that higher-order theorem provers can be applied. Further details are presented in Section 6 (Logic and Philosophy) of the SEP entry on  automated reasoning  and also in  Section 5.2;  moreover, see Benzmüller &amp; Woltzenlogel-Paleo 2014 and Benzmüller 2019.