4
Build-Depends: debhelper (>= 4.0.0)
5
Maintainer: Roland Stigge <stigge@antcom.de>
6
Standards-Version: 3.6.1
10
Depends: ${shlibs:Depends}
11
Description: An automated theorem prover for first-order logic with equality
12
SPASS is a saturation-based automated theorem prover for first-order logic with
13
equality. It is unique due to the combination of the superposition calculus
14
with specific inference/reduction rules for sorts (types) and a splitting rule
15
for case analysis motivated by the beta-rule of analytic tableaux and the case
16
analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a
17
sophisticated clause normal form translation.
19
This package consists of the SPASS/FLOTTER binary, documentation, and a small
20
example collection. The tools collections contain the proof checker pcs, the
21
syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer
24
For more information, additional and partly huge example collections, consider
25
the project homepage at http://spass.mpi-sb.mpg.de/.
added
removed
debian/control
