Paquet : spass (3.9-1.1) [debports]

[ Paquet source :  ]

démonstrateur automatique de théorème pour la logique du premier ordre avec égalité

SPASS est un démonstrateur automatique de théorème basé sur la saturation pour la logique du premier ordre égalitaire. Il est unique à cause de la combinaison de calcul de recouvrement (superposition calculus) avec des règles spécifiques d’inférence ou réduction pour des genres (types) et une règle de dissociation pour l’analyse de cas motivés par une règle bêta de tableaux analytiques et l’analyse de cas employé dans la procédure de Davis-Putnam. De plus, SPASS fournit une traduction sophistiquée de forme normale conjonctive (clause normal form).

Ce paquet consiste en un binaire SPASS/FLOTTER, la documentation et une petite collection d’exemples. La collection d’outils fournit le vérificateur de preuve pcs, les traducteurs de syntaxe dfg2otter et dfg2tptp, et le joli afficheur ASCII dfg2ascii.

Autres paquets associés à spass

• dep: libc6.1 (>= 2.4)

  bibliothèque C GNU : bibliothèques partagées
  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 (portage non officiel)	282,9 ko	1 146,0 ko	[liste des fichiers]