SPASS-XDB - Automated Reasoning with World Knowledge </HEAD> <BODY ALIGN=JUSTIFY> <HR> <H1 ALIGN=CENTER> SPASS-XDB - Automated Reasoning with World Knowledge </H1> <H3> Abstract </H3> There is a growing demand for automated reasoning with <EM>world knowledge</EM>. For example, a reasoning system with knowledge of what cities are located near water, and access to data describing current weather conditions, would be able to predict which cities might be flooded (e.g., by tidal surge). World knowledge is available from a growing number of sources, e.g., online databases, SPARQL endpoints, web services, computational systems, and search engines. Static sources provide a large but finite number of facts, while dynamic and computational sources can provide infinitely many facts by generating them on demand. For deep reasoning, world knowledge is used in conjunction with ontological axioms that describe the structure of the world in which the knowledge resides. Automated Theorem Proving (ATP) systems have traditionally not been well suited to reasoning with world knowledge (where the facts are viewed as positive unit axioms), because they expect to load all the formulae before deduction starts. The large (possibly infinite) number of axioms available from world knowledge sources dictates that the axioms be retrieved dynamically during deduction. SPASS-XDB is an ATP system that incorporates world knowledge axioms from multiple external sources, asynchronously on demand, during its deduction process. This talk describes the general architecture of SPASS-XDB, and provides some details of the most recent developments integrating Mathematica and internet search engines as sources of world knowledge axioms. <P> <HR> </BODY> </HTML>