[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ Quellcode: spass  ]

Paket: spass (2.1-4)

An automated theorem prover for first-order logic with equality

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/.

Andere Pakete mit Bezug zu spass

  • hängt ab von
  • empfiehlt
  • schlägt vor
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    GNU C-Bibliothek: Dynamische Bibliotheken
    auch ein virtuelles Paket, bereitgestellt durch libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    Embedded GNU C Library: Shared libraries
    auch ein virtuelles Paket, bereitgestellt durch libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    Embedded GNU C Library: Shared libraries
    auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [nicht alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    Embedded GNU C Library: Shared libraries
    auch ein virtuelles Paket, bereitgestellt durch libc6.1-udeb

spass herunterladen

Download für alle verfügbaren Architekturen
Architektur Paketgröße Größe (installiert) Dateien
alpha 1 381,7 kB3208 kB [Liste der Dateien]
amd64 1 466,9 kB3084 kB [Liste der Dateien]
armel 1 340,9 kB2864 kB [Liste der Dateien]
avr32 (inoffizielle Portierung) 1 205,0 kB2008 kB [Liste der Dateien]
hppa 1 417,7 kB2936 kB [Liste der Dateien]
hurd-i386 1 258,1 kB2720 kB [Liste der Dateien]
i386 1 262,0 kB2716 kB [Liste der Dateien]
ia64 1 970,3 kB6132 kB [Liste der Dateien]
kfreebsd-amd64 1 467,8 kB3186 kB [Liste der Dateien]
kfreebsd-i386 1 260,8 kB2786 kB [Liste der Dateien]
m68k (inoffizielle Portierung) 1 113,6 kB2600 kB [Liste der Dateien]
mips 1 389,3 kB3716 kB [Liste der Dateien]
mipsel 1 395,1 kB3716 kB [Liste der Dateien]
powerpc 1 408,0 kB3240 kB [Liste der Dateien]
s390 1 391,1 kB2992 kB [Liste der Dateien]
sparc 1 310,4 kB2932 kB [Liste der Dateien]