ATP XDB - External Data Access for ATP

• Access to data (axioms) in databases that are
  • (Effectively) too large to load
  • Computed rather stored
• Cyc, YAGO, Wikipedia, Yahoo Geoservices, BioBike, Arithmetic, Axiom schemas, Lemma generators, MultiNet, Databases, ...
• Limited existing research and implementations

Implementation

• Prototype in simplest setting
  • Positive ground facts
  • TPTP Q&A protocol with SZS standards
  • Local process servers
  • Asynchronous search time pull
• Implemented in SPASS
• Four external data sources
  • TPTP server of TPTP data (Prolog)
  • Real arithmetic compute server (Prolog, TPTP standards)
  • SQL database and SPARQL endpoint server (Java)
  • WWW server (Yahoo MapServices)

Examples

• Find a member of the Curie family who has won two prizes (YAGO)
• Prove that Abraham Lincoln is a mammal (YAGO and SUMO)
• Find a composer born in the first half of the 18th century (YAGO, arithmetic)
• Find an OECD country whose capital is at the same latitude as Moscow, to the nearest degree (YAGO, arithmetic, MapServices)
• Name an actor from the movie Chinatown who was born before Alan Turing (YAGO, LinkedMovieDB, arithmetic)
• Make it play Trivial Pursuit!