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

Пакунок: 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/.

Інші пакунки пов'язані з spass

  • depends
  • recommends
  • suggests
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    Бібліотека GNU C: спільні бібліотеки
    also a virtual package provided by libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    Бібліотека GNU C: спільні бібліотеки
    also a virtual package provided by libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    Бібліотека GNU C: спільні бібліотеки
    also a virtual package provided by libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [not alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    Бібліотека GNU C: спільні бібліотеки
    also a virtual package provided by libc6.1-udeb

Завантажити spass

Завантаження для всіх доступних архітектур
Архітектура Розмір пакунка Розмір після встановлення Файли
alpha 1,381.7 kB3208 kB [список файлів]
amd64 1,466.9 kB3084 kB [список файлів]
armel 1,340.9 kB2864 kB [список файлів]
avr32 (unofficial port) 1,205.0 kB2008 kB [список файлів]
hppa 1,417.7 kB2936 kB [список файлів]
hurd-i386 1,258.1 kB2720 kB [список файлів]
i386 1,262.0 kB2716 kB [список файлів]
ia64 1,970.3 kB6132 kB [список файлів]
kfreebsd-amd64 1,467.8 kB3186 kB [список файлів]
kfreebsd-i386 1,260.8 kB2786 kB [список файлів]
m68k (unofficial port) 1,113.6 kB2600 kB [список файлів]
mips 1,389.3 kB3716 kB [список файлів]
mipsel 1,395.1 kB3716 kB [список файлів]
powerpc 1,408.0 kB3240 kB [список файлів]
s390 1,391.1 kB2992 kB [список файлів]
sparc 1,310.4 kB2932 kB [список файлів]