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