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.
Other Projects
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 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.
