A World of Questions ... A World of Knowledge ... A World of Answers

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.

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