 Fitelson &amp; Zalta 2007, Oppenheimer &amp; Zalta 2011, and Alama, Oppenheimer, &amp; Zalta 2015 describe several applications of automated reasoning in computational metaphysics. By representing formal metaphysical claims as axioms and premises in an automated reasoning environment using programs like Prover9, Mace4, the E-prover system and Paradox, the logical status of metaphysical arguments is investigated. After the suitable formalization of axioms and premises, the model finder program Mace4 is used to help verify their consistency. Then, using Prover9, proofs are automatically generated for a number of theorems of the Theory of Plato’s Forms, twenty five fundamental theorems of the Theory of Possible Worlds, the theorems described in Leibniz’s unpublished paper of 1690 and in his modal metaphysics, and a fully automated construction of Saint Anselm’s Ontological Argument. In the latter application, Saint Anselm is understood in Oppenheimer &amp; Zalta 2011 as having found a way of inferring God’s existence from His mere being as opposed to inferring God’s actuality from His mere possibility. This allows for a formalization that is free of modal operators, involving an underlying logic of descriptions, three non-logical premises, and a definition of God. Here are two key definitions in the formalization, as inputted into Prover9, that helped express the concept of God: 