|
|
File Search | Catalog | Content Search |
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/.
| Homepage: | - |
| Package version: | 3.7-2 |
| Architecture: | ia64 |
| Distribution: | Debian |
| Filename: | spass_3.7-2_ia64.deb |
Welcome to SPASS!
=================
This is the generic README file for all SPASS distributions, so your downloaded
package may only contain a subset of what is described here.
Important Files
===============
INSTALLATION for a guide to install the prover, man pages,
tools etc.; by default binaries are installed
in /usr/local/bin and man-pages in /usr/local/man
more»SPASS(1) SPASS SPASS(1)
NAME
SPASS - automated theorem prover for full first-order logic
with equality
SYNOPSIS
SPASS [options] [inputfile]
DESCRIPTION
SPASS is an automated theorem prover for full sorted first-
order logic with equality that extends superposition by sorts
and a splitting rule for case anal
more»DFG2ASCII(1) SPASS DFG2ASCII(1)
NAME
dfg2ascii - transforms DFG files into pretty printed ASCII
files
SYNOPSIS
dfg2ascii <infile>
DESCRIPTION
dfg2ascii is a program to convert a problem input file in DFG
format into pretty-printed ASCII text. It prints out the
axioms and the conjectures, in that order.
SEE ALSO
more»DFG2DFG(1) SPASS DFG2DFG(1)
NAME
dfg2dfg - calcul
more»DFG2OTTER(1) SPASS DFG2OTTER(1)
NAME
dfg2otter - tran
more»DFG2OTTER.PL(1) SPASS DFG2OTTER.PL(1)
NAME
dfg2otter - tran
more»DFG2TPTP(1) SPASS DFG2TPTP(1)
NAME
dfg2tptp - trans
more»TPTP2DFG(1) SPASS TPTP2DFG(1)
NAME
tptp2dfg - trans
more»| [DIR] | DEBIAN/ (2) 65535+ mirrors | ||
| [DIR] | usr/ (2) 65535+ mirrors |