Computational metaphysics (nonfiction)
Computational metaphysics is a formal, axiomatic metaphysics (i.e., the study of metaphysics using formally represented axioms and premises to derive conclusions) in an automated reasoning environment. It is also the name of an academic project which is developing this formal, axiomatic metaphysics.
The project uses the axiomatic theory of abstract objects developed at the Metaphysics Research Lab at Stanford University.
The project's web site states:
The basic idea is to represent the axioms and definitions of abstract object theory in the syntax of an automated reasoning system. Once this is done, arbitrary propositions in the language of object theory can either be proved or shown to be independent of the basic axioms and definitions. In the past, we have used PROVER9 (and its accompanying model-finding program, MACE4), as our automated reasoning system. (PROVER9 is the successor to OTTER.) This meant representing things in the syntax of PROVER9.
More recently, we have moved to a more generic framework, namely, TPTP syntax, which can be parsed by all current theorem provers and model-finders.
In the News
Fiction cross-reference
Nonfiction cross-reference
External links:
- Computational Metaphysics - project home page @ stanford.edu