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
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.
- 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.
- The slides from the
talk provide an overview.
slide on some testing done illustrates the kinds of questions that
SPASS-XDB can answer.
- SPASS-XDB is available online in the
Here are some inputs that you can cut-and-paste into the interface and
solve using SPASS-XDB ...
- 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
- 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
- Related projects:
SPASS-XDB was conceived of, and originally developed, at the
Automation of Logic
Research Group in the
Max Planck Institut für