##### Wikipedia

**SPASS**

**SPASS** is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for *Synergetic Prover Augmenting Superposition with Sorts*. The theorem proving system is released under the FreeBSD license.

An extension of SPASS called SPASS-XDB added support for on-the-fly retrieval of positive unit axioms from external sources. SPASS-XDB can thus incorporate facts coming from relational databases, web services, or linked data servers. Support for arithmetic using Mathematica was also added.