Steps Toward a Computational Metaphysics
Branden Fitelson and Edward N. Zalta
Journal of Philosophical Logic, 36/2 (April 2007): 227–247.
In this paper, the authors describe their initial investigations in
computational metaphysics. Our method is to implement axiomatic
metaphysics in an automated reasoning system. In this paper, we
describe what we have discovered when the theory of abstract objects
is implemented in PROVER9 (a first-order automated
reasoning system which is the successor to OTTER).
After reviewing the second-order, axiomatic theory of abstract
objects, we show (1) how to represent a fragment of that theory in
PROVER9's first-order syntax, and (2) how
PROVER9 then finds proofs of interesting theorems of metaphysics,
such as that every possible world is maximal. We conclude the paper
by discussing some issues for further research.
[Preprint available online in PDF]