Large Theories and World Knowledge

Large Theories

• Many functors and predicates, many (common) axioms, many theorems
• SUMO, Cyc, Mizar, YAGO, Wikipedia, WordNet, MeSH, DBPedia, CIA Factbook, GenBank ...
• Different challenges for ATP
  • Parsing and building data structures
  • Loading and preprocessing the common axioms only once
  • Selecting axioms that are likely to be useful
  • Extracting heuristics and lemmas from proofs

Infinite Theories

• Dynamic and computational sources of axioms
• Mathematica, HR, XchangeRates, Weather, AGInT, ...
• Infinite number of "axioms"

The State-of-the-Art in ATP

• Large theories only a recent focus
• Few systems can load and reason with millions of axioms
• A finite ATP system cannot load an infinite number of axioms