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

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

Muut pakettiin spass liittyvät paketit

  • depends
  • recommends
  • suggests
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    GNU-C-kirjasto: jaetut kirjastot
    myös näennäispaketti, jonka toteuttaa libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    GNU-C-kirjasto: jaetut kirjastot
    myös näennäispaketti, jonka toteuttaa libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    GNU-C-kirjasto: jaetut kirjastot
    myös näennäispaketti, jonka toteuttaa libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [ei alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    GNU-C-kirjasto: jaetut kirjastot
    myös näennäispaketti, jonka toteuttaa libc6.1-udeb

Imuroi spass

Imurointi kaikille saataville arkkitehtuureille
Arkkitehtuuri Paketin koko Koko asennettuna Tiedostot
alpha 1,381.7 kt3208 kt [tiedostoluettelo]
amd64 1,466.9 kt3084 kt [tiedostoluettelo]
armel 1,340.9 kt2864 kt [tiedostoluettelo]
avr32 (epävirallinen siirros) 1,205.0 kt2008 kt [tiedostoluettelo]
hppa 1,417.7 kt2936 kt [tiedostoluettelo]
hurd-i386 1,258.1 kt2720 kt [tiedostoluettelo]
i386 1,262.0 kt2716 kt [tiedostoluettelo]
ia64 1,970.3 kt6132 kt [tiedostoluettelo]
kfreebsd-amd64 1,467.8 kt3186 kt [tiedostoluettelo]
kfreebsd-i386 1,260.8 kt2786 kt [tiedostoluettelo]
m68k (epävirallinen siirros) 1,113.6 kt2600 kt [tiedostoluettelo]
mips 1,389.3 kt3716 kt [tiedostoluettelo]
mipsel 1,395.1 kt3716 kt [tiedostoluettelo]
powerpc 1,408.0 kt3240 kt [tiedostoluettelo]
s390 1,391.1 kt2992 kt [tiedostoluettelo]
sparc 1,310.4 kt2932 kt [tiedostoluettelo]