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

タグ: 分野: 数学

その他の spass 関連パッケージ

  • 依存
  • 推奨
  • 提案
  • dep: libc0.1 (>= 2.3) [kfreebsd-amd64, kfreebsd-i386]
    GNU C ライブラリ: 共有ライブラリ
    以下のパッケージによって提供される仮想パッケージでもあります: libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    Embedded GNU C Library: Shared libraries
    以下のパッケージによって提供される仮想パッケージでもあります: libc0.3-udeb
  • dep: libc6 (>= 2.5) [avr32]
    Embedded GNU C Library: Shared libraries
    以下のパッケージによって提供される仮想パッケージでもあります: 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]
    Embedded GNU C Library: Shared libraries
    以下のパッケージによって提供される仮想パッケージでもあります: 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 [ファイル一覧]