SPASS-XDB is an extended version of the well-known, state-of-the-art, SPASS automated theorem proving system. The original SPASS reads a problem, consisting of axioms and a conjecture, in TPTP format from a file, and searches for a proof by refutation for the conjecture. SPASS-XDB adds the capability of retrieving extra positive unit axioms (facts) from external sources during the proof search (hence the "XDB", standing for eXternal DataBases). The axioms are retrieved asynchronously, on-demand, based on an expectation that they will contribute to completing the proof. The axioms are retrieved from a range of external sources, including SQL databases, SPARQL endpoints, WWW services, computation sources (e.g., computer algebra systems), etc., using a TPTP standard protocol.

• The basic design and implementation of SPASS-XDB are described in
  Suda M., Sutcliffe G., Wischnewsk P., Lamotte-Schubert M., de Melo G. (2009), External Sources of Axioms in Automated Theorem Proving, Mertsching B., Proceedings of the 32nd Annual Conference on Artificial Intelligence (Paderborn, Germany), Lecture Notes in Artificial Intelligence 5803. pp.281-288. (BibTeX, DOI)

• Control features and applications of SPASS-XDB are described in
  Sutcliffe G., Suda M., Teyssandier A., Dellis N., de Melo G., Progress Towards Effective Automated Reasoning with World Knowledge, Murray C., Lane H., Proceedings of the 23rd International FLAIRS Conference (Daytona Beach, USA), pp.110-115. (BibTeX, Online)

• The slides from the talk provide an overview. The slide on some testing done illustrates the kinds of questions that SPASS-XDB can answer.

• SPASS-XDB is available online in the SystemOnTPTP interface. Here are some inputs that you can cut-and-paste into the interface and solve using SPASS-XDB ... AbeMammal, AlPacino, CloudyCapitals, Composers18thCentury, CuriePrizes, CapitalLevelMoscow, FloodingCopenhagen, ViennaTravel.

• Direct access to some of the external sources of axioms is available online in the System Q&A interface.

• SPASS-XDB has been integrated into the SInE framework, thus allowing focussed use of complex axioms from large knowledge bases, in particular from the Suggested Upper Merged Ontology (SUMO).

• AleXSI is a prototype web interface for building questions that SPASS-XDB is able to (in principle - it's search you know!) answer.

• CNL-WKR is a natural language interface to SPASS-XDB, using Attempto Controlled English (ACE).

• Related projects: Project Halo, PowerAqua, DeepQA, TrueKnowledge, KnowItAll, Cyc, SmartWeb, OpenMind. LogAnswer. MORE.

SPASS-XDB was conceived of, and originally developed, at the Automation of Logic Research Group in the Max Planck Institut für Informatik.