Het bronpakket spass downloaden:
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/.
|
|
|
| Platform | Pakketgrootte | Geïnstalleerde grootte | Bestanden |
|---|---|---|---|
| alpha | 1.381,7 kB | 3208 kB | [overzicht] |
| amd64 | 1.466,9 kB | 3084 kB | [overzicht] |
| armel | 1.340,9 kB | 2864 kB | [overzicht] |
| avr32 (unofficial port) | 1.205,0 kB | 2008 kB | [overzicht] |
| hppa | 1.417,7 kB | 2936 kB | [overzicht] |
| hurd-i386 | 1.258,1 kB | 2720 kB | [overzicht] |
| i386 | 1.262,0 kB | 2716 kB | [overzicht] |
| ia64 | 1.970,3 kB | 6132 kB | [overzicht] |
| kfreebsd-amd64 | 1.467,8 kB | 3186 kB | [overzicht] |
| kfreebsd-i386 | 1.260,8 kB | 2786 kB | [overzicht] |
| m68k (unofficial port) | 1.113,6 kB | 2600 kB | [overzicht] |
| mips | 1.389,3 kB | 3716 kB | [overzicht] |
| mipsel | 1.395,1 kB | 3716 kB | [overzicht] |
| powerpc | 1.408,0 kB | 3240 kB | [overzicht] |
| s390 | 1.391,1 kB | 2992 kB | [overzicht] |
| sparc | 1.310,4 kB | 2932 kB | [overzicht] |