SPASSXDB
A World of Questions ... A World of Knowledge ... A World of Answers
SPASSXDB is an extended version of the wellknown, stateoftheart,
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.
SPASSXDB 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, ondemand, 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 SPASSXDB are described in
Suda M., Sutcliffe G., Wischnewsk P., LamotteSchubert 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.281288.
(BibTeX,
DOI)
 Control features and applications of SPASSXDB 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.110115.
(BibTeX,
Online)
 The slides from the
talk provide an overview.
The
slide on some testing done illustrates the kinds of questions that
SPASSXDB can answer.
 SPASSXDB is available online in the
SystemOnTPTP
interface.
Here are some inputs that you can cutandpaste into the interface and
solve using SPASSXDB ...
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.
 SPASSXDB 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 SPASSXDB is
able to (in principle  it's search you know!) answer.

CNLWKR is a natural language interface to SPASSXDB, using
Attempto Controlled English
(ACE).
 Related projects:
Project Halo,
PowerAqua,
DeepQA,
TrueKnowledge,
KnowItAll,
Cyc,
SmartWeb,
OpenMind.
LogAnswer.
MORE.
SPASSXDB was conceived of, and originally developed, at the
Automation of Logic
Research Group in the
Max Planck Institut für
Informatik.