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