If you are going to use a computer to automatically generate new facts using an ontology
then you have to do fairly sophisticated filtering of the results. If you start with just
a few axioms for logic and Euclidean geometry you could have a computer automatically
prove new theorems using them forever. Most of the results would be boring though. To
identify the gems like the proof that there are only 5 Platonic solids requires you to
analyze the network of results that are produced to find the elegant, interesting, useful,
powerful, surprising, deep, and important ones.
See Wolfram's note on empirical metamathematics:
http://www.wolframscience.com/nksonline/page-1176b-text