/usr/share/doc/spass/README is in spass 3.7-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 | 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;
use the prefix option of make install for a different
path
LICENCE for the licence agreement that you certify by
installation, its the FreeBSD Licence
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.
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-syntax input files.
tptp2dfg translated TPTP-syntax input files into DFG-syntax 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://www.spass-prover.org/
for recent developments, downloads etc.
have SPASS
the SPASS team
|