Imuroi lähdekoodipaketti spass:
SPASS is a saturation-based automated theorem prover for first-order logic with equality. It is unique due to the combination of the superposition calculus with specific inference/reduction rules for sorts (types) and a splitting rule for case analysis motivated by the beta-rule of analytic tableaux and the case analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a sophisticated clause normal form translation.
This package consists of the SPASS/FLOTTER binary, documentation, and a small example collection. The tools collections contain the proof checker pcs, the syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer dfg2ascii.
For more information, additional and partly huge example collections, consider the project homepage at http://spass.mpi-sb.mpg.de/.
|
|
|
| Arkkitehtuuri | Paketin koko | Koko asennettuna | Tiedostot |
|---|---|---|---|
| alpha | 1,381.7 kt | 3208 kt | [tiedostoluettelo] |
| amd64 | 1,466.9 kt | 3084 kt | [tiedostoluettelo] |
| armel | 1,340.9 kt | 2864 kt | [tiedostoluettelo] |
| avr32 (epävirallinen siirros) | 1,205.0 kt | 2008 kt | [tiedostoluettelo] |
| hppa | 1,417.7 kt | 2936 kt | [tiedostoluettelo] |
| hurd-i386 | 1,258.1 kt | 2720 kt | [tiedostoluettelo] |
| i386 | 1,262.0 kt | 2716 kt | [tiedostoluettelo] |
| ia64 | 1,970.3 kt | 6132 kt | [tiedostoluettelo] |
| kfreebsd-amd64 | 1,467.8 kt | 3186 kt | [tiedostoluettelo] |
| kfreebsd-i386 | 1,260.8 kt | 2786 kt | [tiedostoluettelo] |
| m68k (epävirallinen siirros) | 1,113.6 kt | 2600 kt | [tiedostoluettelo] |
| mips | 1,389.3 kt | 3716 kt | [tiedostoluettelo] |
| mipsel | 1,395.1 kt | 3716 kt | [tiedostoluettelo] |
| powerpc | 1,408.0 kt | 3240 kt | [tiedostoluettelo] |
| s390 | 1,391.1 kt | 2992 kt | [tiedostoluettelo] |
| sparc | 1,310.4 kt | 2932 kt | [tiedostoluettelo] |