diff options
Diffstat (limited to 'test/spass/README')
| -rw-r--r-- | test/spass/README | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/test/spass/README b/test/spass/README new file mode 100644 index 0000000..efdfb84 --- /dev/null +++ b/test/spass/README @@ -0,0 +1,96 @@ + 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 + =============== + +AUTHORS all authors that contributed to SPASS + +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; + use the prefix option of make install for a different + path + +COPYING for the licence agreement that you certify by + installation, its the GNU GENERAL PUBLIC LICENSE, Version 2 + +VERSIONHISTORY changes starting from version 1.0.0 + +README is this file + + + + + Programs + ======== + +The distribution contains the following programs. Most +of them give you a brief description if they are called +without arguments. Most of the programs come with man-pages. + +SPASS is our prover for first-order logic with equality. + +FLOTTER translates first-order formulae into clauses; its + incorporated in SPASS and hence now only a link to + SPASS. + +pcs is our proof checker. NOTE that in its default settings + pcs needs an installation of otter for proof checking. + You can also employ SPASS itself for this purpose by the + -o option. + +pgen generates out of a SPASS proof file all subtasks needed + to guarantee the correctness of the proof. + +dfg2otter translates DFG-syntax input files into otter input files, + without any settings commands. + +dfg2otter.pl has the same functionality than dfg2otter but adds specific + settings that are useful if otter is employd as a proof checker + for SPASS. + +dfg2tptp translates DFG-syntax input files into TPTP input files. + + +dfg2ascii provides an ASCII pretty print of DFG-syntax input files + + + Documentation + ============= + +Besides the man pages, in the directory doc you'll find a description +of our input syntax (spass-input-syntax.pdf), a small tutorial (tutorial.pdf) +that is just a print out of our tutorial web page and the complete +theory of SPASS (handbook-spass.pdf). Furthermore, there is a FAQ +database (faq.txt). + + + Examples + ======== + +In the examples directory you'll find some small examples. Further +example collections can be downloaded from the SPASS homepage. By +convention, files ending in ".dfg" are formula files and files ending +in ".cnf" are files containing clauses. + + + WWW + === + +Consider the SPASS homepage at + + http://spass.mpi-sb.mpg.de/ + +for recent developments, downloads etc. + + + + + +have SPASS + Christoph Weidenbach
\ No newline at end of file |