| Paketname | spass |
| Beschreibung | An automated theorem prover for first-order logic with equality |
| Archiv/Repository | Offizielles Debian Archiv squeeze (main) |
| Version | 3.7-2 |
| Sektion | science |
| Priorität | optional |
| Installierte Größe | 3936 Byte |
| Hängt ab von | dpkg (>= 1.15.4) | install-info, libc6 (>= 2.3) |
| Empfohlene Pakete | |
| Paketbetreuer | Roland Stigge |
| Quelle | |
| Paketgröße | 2076024 Byte |
| Prüfsumme MD5 | 617884c8071be1ac072c8a143befb6e0 |
| Prüfsumme SHA1 | 27d1e58570865b753b68d356717f5135ae84e8ce |
| Prüfsumme SHA256 | e5db40238504c64dcf8b429d5bc2e6a0452ef96f7d0b6a34e63762d12ec9e0ff |
| Link zum Herunterladen | spass_3.7-2_i386.deb |
| Ausführliche Beschreibung | 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/.
|