Automation of Logic
English

Download Binaries/Libraries/Sources of SPASS for your platform right now!

The SPASS binary/source distributions consists of a SPASS/FLOTTER binary, documentation, a small example collection and the tools dfg2otter, dfg2tptp, tptp2dfg, and the ASCII pretty printer dfg2ascii.

For additional, partly huge example collections, consider the problem libraries. For easy compilation of the sources, the GNU gcc compiler should be available. For all categories, download and unpack the gziped tar files and follow the instructions in the contained README files.

The Windows 2000/XP as well as the MAC distribution is a self extracting archive that automatically starts an install shield. Starting from version 3.5 we move from Qt to a Java set up for the GUI.

SPASS 3.9 Linux Sources

  • Linux sources of SPASS 3.9 and the tools (.tgz 0.5MB). The difference to version 3.7 are some bug fixes plus the ability to parse large input files.

SPASS 3.5 Binaries

  • PC Linux 2.X.X 32-Bit (.tgz 1.4MB), PC Linux 2.X.X 64-Bit (.tgz 1.6MB)
  • Windows XP inlcuding QT based GUI (.exe 6.2MB)
  • Windows XP inlcuding Java based GUI (.exe 1.2MB)
  • MAC OS X86 (.dmg 1.7MB)

CD-ROM Image 3.5

  • Windows XP including new GUI, sources and libraries in preparation.

Problem Libraries

  • The Royle Sudoku puzzles translated into dfg syntax (.tgz 338MB) as well as translator plus original puzzles (.tgz 574KB)
  • The Pelletier Collection (.tgz 5KB)
  • The Neuman-Stubblebine Security Protocol Analysis Version 1.1 (.tgz 1KB)
  • Software Reuse of List Functions Version 5 (.tgz 376KB) generated in the HAMMR project by Bernd Fischer.
  • TPTP Version 3.1.0 in SPASS Syntax (.tgz 11.47MB) generated out of the TPTP problem library maintained by Geoff Sutcliffe and Christian Suttner.

SPASS 3.7 Sources

  • Sources of SPASS 3.7 and the tools (.tgz 1.3MB). The difference to version 3.5 are minor bug fixes with respect to flag usage. Compiling the sources may create a number of warnings; don't worry, in particular, the code is 64-Bit clean and we will beautify it to get rid of the warnings for the next release.

Changes compared to version 3.0

  • Moved distribution to the FreeBSD Licence.
  • Joined the flags -PCRW und -PREW into the latter, renamed -QuantExch into -CNFQuantExch.
  • For Linux binaries SPASS now always respects a given time limit.
  • Moved to a fair and eager splitting heuristic. The new flag -SplitMinInst, sets the minimal average number of instances of all split atoms of a split in order to perfrom the split and is increased after each subsequent split and reset after performance of a different inference. Propositional non-Horn clauses are always split. Removed the flag -SplitHeuristic.
  • Reimplemented the conjunctive normal form algorithm of FLOTTER.
  • Added printing of the number of performed splits to the output.
  • Added improved split backtracking where also the split information of a left branch refutation is stored and then compared to the split information of the corresponding right branch, potentially leading to a more aggressive branch condensing. See the papers on Splitting by Fietzke and Weidenbach.
  • Added subterm contextual rewriting with fault caching. See the man page and the corresponding papers by Weidenbach & Wischnewski.
  • Added support for XOR, NAND, NOR and special symbol for NOT EQUAL to DFG syntax.
  • Added new translator tptp2dfg from TPTP syntax to DFG syntax. See the man page.
  • Added include directives to the SPASS DFG input syntax. For more information see the syntax description.
  • Removed a bunch of compile time constants hindering handling of large files.
  • Added native TPTP syntax support, controlled by the -TPTP flag.
  • Moved from a sort theory module considering residues to a purely declaration based sort theory.
  • New self written command line parser.
  • Added the flags -CNFSub, -CNFCon, -CNFRedTimeLimit to FLOTTER that control the use of subsumption, condensing and the overall time for reduction during cnf transformation. See the man pages for further details.
  • Added rewriting with unoriented equations to forward and backward rewriting. Until Version 3.0 only for unit equations both directions were implemented.
  • Fixed all known bugs.

Previous versions

  • Version 1.0.0: SPASS PC Linux 2.X.X (.tgz 383KB), SPASS Sun Sparc Solaris 5.5 (.tgz 413KB), SPASS Sun Sparc Solaris 5.6 (.tgz 447KB), SPASS Sun X86 Solaris 5.6 (.tgz 402KB), Tools PC Linux 2.X.X (.tgz 600KB), Tools Sun Sparc Solaris 5.5 (.tgz 600KB), Tools Sun Sparc Solaris 5.6 (.tgz 600KB), Tools Sun X86 Solaris 5.6 (.tgz 600KB), SPASS Windows 95/98/NT (.exe 1160KB), Sources Tools & SPASS 1.0.0 (.tgz 529KB)
  • Version 1.0.3: SPASS PC Linux 2.X.X (.tgz 383KB), SPASS Sun Sparc Solaris 5.5 (.tgz 413KB), SPASS Sun Sparc Solaris 5.6 (.tgz 447KB), SPASS Sun X86 Solaris 5.6 (.tgz 402KB), Tools PC Linux 2.X.X (.tgz 600KB), Tools Sun Sparc Solaris 5.5 (.tgz 600KB), Tools Sun Sparc Solaris 5.6 (.tgz 600KB), Tools Sun X86 Solaris 5.6 (.tgz 600KB), Sources Tools & SPASS 1.0.3 (.tgz 529KB)
  • Version 2.0: SPASS PC Linux 2.X.X (.tgz 585KB), SPASS Sun Sparc Solaris 5.8 (.tgz 607KB), SPASS Windows 95/98/NT/2000 (.tgz 2633KB), Tools PC Linux 2.X.X (.tgz 630KB), Tools Sun Sparc Solaris 5.8 (.tgz 715KB), Sources Tools & SPASS 2.0 (.tgz 867KB)
  • Version 2.1: SPASS PC Linux 2.X.X (.tgz 572KB), SPASS Sun Sparc Solaris 5.9 (.tgz 615KB), SPASS Windows 95/98/NT/2000 (.tgz 2617KB), Tools PC Linux 2.X.X (.tgz 592KB), Tools Sun Sparc Solaris 5.9 (.tgz 725KB), Windows 95/98/NT/XP/2000/XP ISO image including sources (.bz2 68984KB), Sources Tools & SPASS 2.1 (.tgz 895KB)
  • Version 2.2: PC Linux 2.X.X (.tgz 1.23MB), Qt for the GUI (Linux, Solaris) (.tgz 19.21MB), Sun Sparc Solaris 5.9 (.tgz 1.39MB), Windows 2000/XP (.exe 1.7MB), Qt for Windows binaries (.exe 35.41MB), Qt for Windows sources (.zip 24.66MB), CD-ROM Image for Windows (.bz2 65.57MB), MAC OS (.dmg 1.57MB), Qt for MAC (.tgz 19.2MB), Sources (.tgz 1.05MB)
  • Version 3.0: PC Linux 2.X.X (.tgz 1.5MB), Qt for Linux Sources (.tgz 27.1MB), Windows 2000/XP (.exe 5.6MB), Qt for Windows Sources (.exe 46.2MB), MAC OS Power PC (.dmg 4.6MB), Qt for MAC Power PC Sources (.tgz 27.1MB), MAC OS Power X86 (.dmg 6.3MB), Qt for MAC Power X86 Sources (.tgz 38.6MB), CD-ROM Image for Windows (.bz2 25.7MB), Nokia N800 choosing the link "http://spass.mpi-inf.mpg.de/download/n800/" to install the package from the N800 application manager using distribution "bora" and components "free", Sources (.tgz 1.2MB)