Useful Links related to SPASS!

Related Projects

An alternative GUI has been written by Mauro Mereu from Milano University. You can obtain it here.
In the context of the Isabelle sledge hammer effort, SPASS is used as first-order automatic tactic, aiming at solving subgoals out of higher-order logic proof attempts.
The temporal logic prover TSPASS developled by Michel Ludwig in Liverpool is based on SPASS.

The father of all todays modern theorem provers is Otter developed by Bill McCune. We use Otter as a single step proof checker for our proof checking tools.
The Darwin prover is a first-order generalization of the Davis-Putnam-Logeman-Loveland procedure, called model evolution, developed by Peter Baumgartner, Alexander Fuchs, and Cesare Tinelli.
The TPTP problem library contains several thousand automated theorem proving problems from various domains (see also the download area). It is maintained by Geoff Sutcliffe and also offers an interface to run various provers(including SPASS) on the TPTP.
One of the very best systems for purely equational reasoning is the Waldmeister theorem prover developed at the Max Planck Institute for Informatics.
The equational theorem prover E, developed by Stephan Schulz
The Vampire theorem prover, developed by Andrei Voronkov
The extension SPASS+T developed by Uwe Waldmann extends SPASS with black box reasoning capabilities for arithmetic theories.