SPASS-XDB - World Knowledge for ATP

Reasoning with world knowledge
- (Effectively) too large to load ... Cyc, YAGO, Wikipedia, BioBike, WordNet, MeSH, DBPedia, CIA Factbook ...
- Computed rather than stored ... Arithmetic, Axiom schemas, Lemma generators, Yahoo GeoServices, GenBank, XchangeRates, Mathmatica, HR, ...
Limited existing research and implementations

Retrieve external data on demand
- Positive ground facts
- Retrieved asynchronously, on demand, during deduction
- TPTP Q&A protocol with SZS standards
- Local mediators for external sources
Implemented in SPASS
A range of external sources
(available online at tptp.org/cgi-bin/SystemQATPTP)

Prove that Abraham Lincoln is a mammal
Find bordering European countries with equally cloudy capitals
Name a composer born in the first half of the 18th century
Name an Al Pacino movie that contains the name "Glen" twice
Name a member of the Curie family who has won two prizes
Name all prizes won by members of the Curie family
Prove it is possible to travel by land from Vienna to Budapest
Name an OECD country's capital that is at the same latitude as Moscow (to the nearest degree)
... and that could get flooded