Welcome to the Classic SPASS Home Page!
Classic SPASS: An Automated Theorem Prover for First-Order Logic with Equality
These pages document the classic SPASS first-order theorem prover up to version 3.9. Starting from version 4.0 SPASS is distributed via the SPASS workbench.
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.
The Classic SPASS www-pages offer to you
- a tutorial to the prover
- 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.
Have SPASS