[ Source: spass ]
Package: spass (3.9-1.1)
Links for spass
Debian Resources:
Download Source Package spass:
Maintainers:
External Resources:
- Homepage [www.mpi-inf.mpg.de]
Similar packages:
Automatiseret læresætningsbeviser for første orden logik med ligestilling
SPASS er en mætningsbaseret automatiseret læresætningsbeviser for første ordens logik med ligestilling. Det er unikt på grund af kombinationen af superposition calculus med særlige regler følgeslutning/reduktion for sortering (typer) og en opsplitningsregel for tilfældeanalyse motiveret af beta-reglen om analytiske tableauer og sagsanalyse anvendt i Davis-Putnam-proceduren. Endvidere tilbyder SPASS en sofistikeret klausulnormalformsoversættelse.
Denne pakke består af den SPASS/FLOTTER-binære fil, dokumentation og en lille eksempelsamling. Værktøjssamlingerne indeholder beviskontrol-pcs, syntaksoversætterne dfg2otter og dfg2tptp og ASCII pretty-printeren dfg2ascii.
Other Packages Related to spass
|
|
|
|
-
- dep: libc6 (>= 2.17)
- GNU C-bibliotek: Delte biblioteker
also a virtual package provided by libc6-udeb
Download spass
| Architecture | Package Size | Installed Size | Files |
|---|---|---|---|
| ppc64el | 301.8 kB | 1,106.0 kB | [list of files] |