 One of the major advances in computational philosophy has been the application of theorem-provers to the analysis of classical philosophical positions and arguments. From axioms of a metaphysical object theory, Zalta and his collaborators use Prover9 and Mace to establish theorems regarding possible worlds, such as the claim that every possible world is maximal, modal theorems in Leibniz, and consequences from Plato’s theory of Forms (Fitelson &amp; Zalta 2007; Alama, Oppenheimer, &amp; Zalta 2015; Kirchner, Benzmüller, &amp; Zalta 2019).