[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ Paquet source : spass  ]

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

Autres paquets associés à spass

  • dépendances
  • recommandations
  • suggestions
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    bibliothèque C GNU : bibliothèques partagées
    un paquet virtuel est également fourni par libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    Embedded GNU C Library: Shared libraries
    un paquet virtuel est également fourni par libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    Embedded GNU C Library: Shared libraries
    un paquet virtuel est également fourni par libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [non alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    Embedded GNU C Library: Shared libraries
    un paquet virtuel est également fourni par libc6.1-udeb

Télécharger spass

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
alpha 1 381,7 ko3208 ko [liste des fichiers]
amd64 1 466,9 ko3084 ko [liste des fichiers]
armel 1 340,9 ko2864 ko [liste des fichiers]
avr32 (portage non officiel) 1 205,0 ko2008 ko [liste des fichiers]
hppa 1 417,7 ko2936 ko [liste des fichiers]
hurd-i386 1 258,1 ko2720 ko [liste des fichiers]
i386 1 262,0 ko2716 ko [liste des fichiers]
ia64 1 970,3 ko6132 ko [liste des fichiers]
kfreebsd-amd64 1 467,8 ko3186 ko [liste des fichiers]
kfreebsd-i386 1 260,8 ko2786 ko [liste des fichiers]
m68k (portage non officiel) 1 113,6 ko2600 ko [liste des fichiers]
mips 1 389,3 ko3716 ko [liste des fichiers]
mipsel 1 395,1 ko3716 ko [liste des fichiers]
powerpc 1 408,0 ko3240 ko [liste des fichiers]
s390 1 391,1 ko2992 ko [liste des fichiers]
sparc 1 310,4 ko2932 ko [liste des fichiers]