» Ubuntu » Packages » lucid (10.04LTS) » science » spass
lucid  ] [  precise  ] [  trusty  ] [  utopic  ] [  vivid  ]
[ Source: spass  ]

Package: spass (2.1-4) [universe]

Links for spass


Ubuntu Resources:

Download Source Package spass:


Please consider filing a bug or asking a question via Launchpad before contacting the maintainer directly.

Original Maintainer (usually from Debian):

  • Roland Stigge

It should generally not be necessary for users to contact the original maintainer.

Similar packages:

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

Other Packages Related to spass

  • depends
  • recommends
  • suggests
  • enhances
  • dep: libc6 (>= 2.4)
    Embedded GNU C Library: Shared libraries
    also a virtual package provided by libc6-udeb

Download spass

Download for all available architectures
Architecture Package Size Installed Size Files
amd64 1,468.3 kB3,096.0 kB [list of files]
i386 1,262.8 kB2,732.0 kB [list of files]