blob: efdfb84f1ebd35beec890e64367048cfe74f5528 (
plain)
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
91
92
93
94
95
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
|
