File: control

package info (click to toggle)
spass 3.7-4
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 5,536 kB
  • ctags: 5,976
  • sloc: ansic: 50,634; yacc: 3,038; sh: 1,079; lex: 430; perl: 407; makefile: 338
file content (26 lines) | stat: -rw-r--r-- 1,399 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
Source: spass
Section: science
Priority: optional
Build-Depends: debhelper (>= 10)
Maintainer: Debian Science Maintainers <debian-science-maintainers@lists.alioth.debian.org>
Uploaders: Ralf Treinen <treinen@debian.org>
Vcs-Git: https://anonscm.debian.org/git/debian-science/packages/spass.git
Vcs-Browser: https://anonscm.debian.org/cgit/debian-science/packages/spass.git
Homepage: http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/
Standards-Version: 3.9.8

Package: spass
Architecture: any
Depends: dpkg (>= 1.15.4) | install-info, ${shlibs:Depends}, ${misc:Depends}
Description: 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.