I am repulsed, appalled, and fascinated.

Computational metaphysics, as we practice it, is the implementation of axiomatic metaphysics in an automated reasoning environment. As our axiomatic metaphysics, we work within the axiomatic theory of abstract objects developed at the Metaphysics Research Lab at Stanford University. As our automated reasoning engine, we currently use PROVER9 (and its accompanying model-finding program, MACE4), but others, such as OTTER are possible.

They go on, on this page, to apply reasoning engines to the Third Man Argument Problem Thinget.