all options
bullseye  ] [  bookworm  ] [  trixie  ] [  sid  ]
[ Source: spass  ]

Package: spass (3.9-1.1)

Links for spass

Screenshot

Debian Resources:

Download Source Package spass:

Maintainers:

External Resources:

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.

Tags: Field: Mathematics

Other Packages Related to spass

  • depends
  • recommends
  • suggests
  • enhances

Download spass

Download for all available architectures
Architecture Package Size Installed Size Files
s390x 256.8 kB834.0 kB [list of files]