Package: spass (3.9-1.1 and others)

[ Source: spass  ]

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

• dep: libc6 (>= 2.14) [amd64]

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

  dep: libc6 (>= 2.17) [arm64, ppc64el]

  dep: libc6 (>= 2.3.4) [i386, mips64el]

  dep: libc6 (>= 2.34) [riscv64]

  dep: libc6 (>= 2.4) [armel, armhf, s390x]

Download spass

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
amd64	3.9-1.1	286.2 kB	758.0 kB	[list of files]
arm64	3.9-1.1	245.6 kB	734.0 kB	[list of files]
armel	3.9-1.1	209.1 kB	601.0 kB	[list of files]
armhf	3.9-1.1	218.7 kB	425.0 kB	[list of files]
i386	3.9-1.1	321.2 kB	981.0 kB	[list of files]
mips64el	3.9-1.1	251.3 kB	1,042.0 kB	[list of files]
ppc64el	3.9-1.1	301.8 kB	1,106.0 kB	[list of files]
riscv64	3.9-1.1+b1	275.6 kB	583.0 kB	[list of files]
s390x	3.9-1.1	256.8 kB	834.0 kB	[list of files]