SPASS je automatizovaný teorém první logiky týkající se rovnosti. Díky kombinaci superpozičního výpočtového aparátu se specifickými pravidly odvozování/redukce jednotlivých typů a dělícími pravidly pro případovou analýzu motivovanou beta-pravidly analytických obrazů a analýzou případů procedury Davis-Putnamovi. Kromě toho, SPASS obsahuje sofistikovanou klauzuli překladu normálních forem.
Tento balíček se skládá z binárky SPASS/FLOTTER, dokumentace a malé kolekce příkladů. Nástroje obsahují kontrolní mechanismus, překlad syntaxe dfg2otter, dfg2tptp a pěkný tisk dfg2ascii.
Pro více informací, doplňků a další příklady se podívejte na domovskou stránku projektu na adrese http://spass.mpi-sb.mpg.de/.
|
|
|
| Architecture | Package Size | Installed Size | Files |
|---|---|---|---|
| alpha | 1,381.7 kB | 3208 kB | [list of files] |
| amd64 | 1,466.9 kB | 3084 kB | [list of files] |
| armel | 1,340.9 kB | 2864 kB | [list of files] |
| avr32 (unofficial port) | 1,205.0 kB | 2008 kB | [list of files] |
| hppa | 1,417.7 kB | 2936 kB | [list of files] |
| hurd-i386 | 1,258.1 kB | 2720 kB | [list of files] |
| i386 | 1,262.0 kB | 2716 kB | [list of files] |
| ia64 | 1,970.3 kB | 6132 kB | [list of files] |
| kfreebsd-amd64 | 1,467.8 kB | 3186 kB | [list of files] |
| kfreebsd-i386 | 1,260.8 kB | 2786 kB | [list of files] |
| m68k (unofficial port) | 1,113.6 kB | 2600 kB | [list of files] |
| mips | 1,389.3 kB | 3716 kB | [list of files] |
| mipsel | 1,395.1 kB | 3716 kB | [list of files] |
| powerpc | 1,408.0 kB | 3240 kB | [list of files] |
| s390 | 1,391.1 kB | 2992 kB | [list of files] |
| sparc | 1,310.4 kB | 2932 kB | [list of files] |