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

Balík: 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/.

Ostatné balíky súvisiace s balíkom spass

  • závisí
  • odporúča
  • navrhuje
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    knižnica GNU C - zdieľané knižnice
    tiež virtuálny balík poskytovaný balíkom libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    knižnica GNU C - zdieľané knižnice
    tiež virtuálny balík poskytovaný balíkom libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    knižnica GNU C - zdieľané knižnice
    tiež virtuálny balík poskytovaný balíkom libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [nie alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    knižnica GNU C - zdieľané knižnice
    tiež virtuálny balík poskytovaný balíkom libc6.1-udeb

Stiahnuť spass

Stiahnuť pre všetky dostupné architektúry
Architektúra Veľkosť balíka Nainštalovaná veľkosť Súbory
alpha 1,381.7 kB3208 kB [zoznam súborov]
amd64 1,466.9 kB3084 kB [zoznam súborov]
armel 1,340.9 kB2864 kB [zoznam súborov]
avr32 (neoficiálny port) 1,205.0 kB2008 kB [zoznam súborov]
hppa 1,417.7 kB2936 kB [zoznam súborov]
hurd-i386 1,258.1 kB2720 kB [zoznam súborov]
i386 1,262.0 kB2716 kB [zoznam súborov]
ia64 1,970.3 kB6132 kB [zoznam súborov]
kfreebsd-amd64 1,467.8 kB3186 kB [zoznam súborov]
kfreebsd-i386 1,260.8 kB2786 kB [zoznam súborov]
m68k (neoficiálny port) 1,113.6 kB2600 kB [zoznam súborov]
mips 1,389.3 kB3716 kB [zoznam súborov]
mipsel 1,395.1 kB3716 kB [zoznam súborov]
powerpc 1,408.0 kB3240 kB [zoznam súborov]
s390 1,391.1 kB2992 kB [zoznam súborov]
sparc 1,310.4 kB2932 kB [zoznam súborov]