[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ 源代码: spass  ]

软件包: spass (2.1-4)

An automated theorem prover for first-order logic with equality

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/.

标签: Field: 数学

其它与 spass 有关的软件包

  • 依赖
  • 推荐
  • 建议
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    GNU C 语言运行库：共享库
    同时作为一个虚包由这些包填实: libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    GNU C 语言运行库：共享库
    同时作为一个虚包由这些包填实: libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    GNU C 语言运行库：共享库
    同时作为一个虚包由这些包填实: libc6-udeb
    dep: libc6 (>= 2.5-5) [m68k]
    dep: libc6 (>= 2.7-1) [除 alpha, avr32, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    GNU C 语言运行库：共享库
    同时作为一个虚包由这些包填实: libc6.1-udeb

下载 spass

下载可用于所有硬件架构的
硬件架构 软件包大小 安装后大小 文件
alpha 1,381.7 kB3208 kB [文件列表]
amd64 1,466.9 kB3084 kB [文件列表]
armel 1,340.9 kB2864 kB [文件列表]
avr32 (非官方移植版) 1,205.0 kB2008 kB [文件列表]
hppa 1,417.7 kB2936 kB [文件列表]
hurd-i386 1,258.1 kB2720 kB [文件列表]
i386 1,262.0 kB2716 kB [文件列表]
ia64 1,970.3 kB6132 kB [文件列表]
kfreebsd-amd64 1,467.8 kB3186 kB [文件列表]
kfreebsd-i386 1,260.8 kB2786 kB [文件列表]
m68k (非官方移植版) 1,113.6 kB2600 kB [文件列表]
mips 1,389.3 kB3716 kB [文件列表]
mipsel 1,395.1 kB3716 kB [文件列表]
powerpc 1,408.0 kB3240 kB [文件列表]
s390 1,391.1 kB2992 kB [文件列表]
sparc 1,310.4 kB2932 kB [文件列表]