toutes les options
squeeze  ] [  wheezy  ] [  sid  ]
[ Paquet source : spass  ]

Paquet : spass (3.7-3)

Liens pour spass

Screenshot

Ressources Debian :

Télécharger le paquet source spass :

Responsable :

Paquets similaires :

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

Télécharger spass

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
amd64 2 213,3 ko4 304,0 ko [liste des fichiers]
armel 2 022,3 ko3 864,0 ko [liste des fichiers]
armhf 1 936,0 ko3 053,0 ko [liste des fichiers]
i386 2 085,3 ko4 180,0 ko [liste des fichiers]
ia64 3 015,3 ko7 940,0 ko [liste des fichiers]
kfreebsd-amd64 2 213,3 ko4 396,0 ko [liste des fichiers]
kfreebsd-i386 2 082,9 ko4 252,0 ko [liste des fichiers]
mips 2 028,1 ko4 320,0 ko [liste des fichiers]
mipsel 2 033,9 ko4 320,0 ko [liste des fichiers]
powerpc 2 076,6 ko4 156,0 ko [liste des fichiers]
s390 2 125,0 ko4 252,0 ko [liste des fichiers]
s390x 2 250,4 ko4 610,0 ko [liste des fichiers]
sparc 2 047,6 ko4 024,0 ko [liste des fichiers]