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.