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
- a tutorial to the prover
- a functional but resource restricted web interface to SPASS called WebSPASS
- a download area containing the complete sources and binaries for various platforms, including a native 2000/XP and a MAC version with a neat GUI
- a prototype and experiments
area where we give access to recent SPASS developments and experiments
- links to projects that are related to SPASS as well as to other theorem-provers
- the SPASS (Hi)Story, including information on the prover, people who work(ed) in the project and on our great (bitey and fishy) logo
- ways to contact us; we highly appreciate comments, bug reports etc.
News: Friday, May 28: SPASS 3.5/3.7 mac binaries and windows binaries with new GUI available.
Have SPASS
The SPASS Team
