There exists a modal logic interface to SPASS called MSPASS. The interface is developed at the university of Manchester by Renate Schmidt and Ullrich Hustadt.
An alternative GUI has been written by Mauro Mereu from Milano University. You can obtain it here.
At the computer linguistics department at the Saarland University, Johan Boos uses SPASS to solve problems in the context of natural language understanding. He offers an interface where you can type in a natural language sentence in the discourse of a short story related to the movie Pulp Fiction and then the sentence is interpreted by the help of SPASS.
The Omega project headed by Jörg Siekmann at the computer science department at the Saarland University builds a mathematical proof assistant where SPASS is used as an external reasoner.
Reuse of components is a hot topic in software engineering. In the HAMMR project at the university of Braunschweig, Bernd Fischer successfully used SPASS for this task. Bernd is now working at NASA. The group of Gregor Snelting has moved from Braunschweig to Passsau.
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 FDPLL prover is a first-order version of the Davis-Putnam-Logeman-Loveland procedure, developed by Peter Baumgartner at the University of Koblenz.
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 Christian Suttner and also offers an interface to run various provers(including SPASS) on the TPTP.
