Package: spass (3.9-1.1) [debports]

Links for spass

Debian Resources:

Bug Reports

Download Source Package :

Not found

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

depends

recommends

suggests

enhances

dep: libc6 (>= 2.3.4)

GNU C-bibliotek: Delte biblioteker
also a virtual package provided by libc6-udeb

Download spass

Download for all available architectures
Architecture	Package Size	Installed Size	Files
sparc64 (unofficial port)	212.1 kB	661.0 kB	[list of files]