In the past decades, several emendations of Gödel's (resp. Scott's) modal ontological argument have been proposed, many of which preserve the intended conclusion (the necessary existence of God), while avoiding a controversial side result of the Gödel/Scott variant called the "modal collapse", which expresses that there are no contingent truths (everything is determined, there is no free will). In this paper we provide a summary on recent computer-supported verification studies on some of these modern variants of the ontological argument. The purpose is to provide further evidence that the interaction with the computer technology, which we have developed together with colleagues over the past years, can not only enable the formal assessment of onotological arguments, but can, in fact, help to sharpen our conceptual understanding of the notions and concepts involved. From a more abstract perspective, we claim that interreligious understanding may be fostered by means of formal argumentation and, in particular, formal logical anaylsis supported by modern interactive and automated theorem proving technology.