max planck institut
mpii logo Minerva of the Max Planck Society

Welcome to the SPASS Home Page!

SPASS: An Automated Theorem Prover for First-Order Logic with Equality

If you are interested in first-order logic theorem proving, the formal analysis of software, systems, protocols, formal approaches to AI planning, decision procedures, modal logic theorem proving, SPASS may offer you the right functionality.

If you are interested in sex, drugs, rock'n roll or fish, even though our logo contains a nice drawing of Opistognathus Latitabunda, you may be disappointed by the performance of SPASS.

The SPASS www-pages offer to you

News: Friday, May 28: SPASS 3.5/3.7 mac binaries and windows binaries with new GUI available.


The SPASS Team