SRASS

SRASS is a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a conjecture. The selection is determined by semantics of the axioms and conjecture, ordered heuristically by a syntactic relevance measure. The system is able to solve many problems that cannot be solved alone by the underlying conventional automated reasoning system.

SRASS has been created by:

Geoff Sutcliffe - Loved the basic idea in Petr Pudlak's PhD, and wrote the program.
Yury Puzis - Wrote the Prophet system for measuring the syntactic relevance of axioms with respect to a conjecture.
The developers of the various ATP systems used in the SRASS process: Stephan Schulz (E and EP), Alex Fuchs (FMDarwin), Koen Claessen (Paradox), and the SPASS people (SPASS).

SRASS is available for use online via the System on TPTP interface.