[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ Источник: spass  ]

Пакет: spass (2.1-3)

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: libc6 (>= 2.3.1-1) [hppa]
    библиотека GNU C: динамически подключаемые библиотеки
    также виртуальный пакет, предоставляемый libc6-udeb
    dep: libc6 (>= 2.3.2-1) [не alpha, amd64, hppa, ia64]
    dep: libc6 (>= 2.3.5-1) [amd64]
  • dep: libc6.1 (>= 2.3.2-1) [alpha, ia64]
    библиотека GNU C: динамически подключаемые библиотеки
    также виртуальный пакет, предоставляемый libc6.1-udeb

Загрузка spass

Загрузить для всех доступных архитектур
Архитектура Размер пакета В установленном виде Файлы
alpha 1 433,3 Кб2912 Кб [список файлов]
amd64 1 169,0 Кб2312 Кб [список файлов]
arm 1 076,3 Кб2164 Кб [список файлов]
hppa 1 215,2 Кб2372 Кб [список файлов]
i386 1 068,4 Кб2188 Кб [список файлов]
ia64 1 793,2 Кб4236 Кб [список файлов]
mips 1 204,3 Кб3364 Кб [список файлов]
mipsel 1 200,8 Кб3364 Кб [список файлов]
powerpc 1 213,6 Кб2392 Кб [список файлов]
s390 1 168,6 Кб2436 Кб [список файлов]
sparc 1 108,2 Кб2200 Кб [список файлов]