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
_______________________________________________ Wikidata-l mailing list [email protected] https://lists.wikimedia.org/mailman/listinfo/wikidata-l
