problem-set/algebra/README
created : 08/15/88
revised : 06/30/89

Contents of 'algebra' :
-----------------------

Main File Headings
----------------------------------------------------------------------

README : You are currently here; a description of all the files in
	the directory problem-set/algebra.

Sub-Directories
----------------------------------------------------------------------

boolean : problems in boolean algebras.

category.theory : problems in category theory.

groups : group theory problems.

henkin.models : henkin model problems.

lattices : problems in modular lattices.

rings : ring theory problems.

----------------------------------------------------------------------

For each problem, there are several standard files, which include one
probname.desc file and at least one of each of probname.ver#.in,
probname.ver#.clauses, and probname.ver#.out.  These contain the
following: 

probname.desc : contains the Natural Language Description of the
	problem, where available, credits for problem formulation, 
	and complete details on each formulation and each version.  

probname.ver#.in : contains the problem specification, input clauses, and
	strategy for OTTER; this file is ready to run.

probname.ver#.clauses : contains the description, commentary, and the
	actual clauses (including the denial of the conclusion) used for
	probname.ver#.in, without any strategy; note that comments always are 
	on lines beginning with a %, preceding the clauses to which they
	refer, and that clauses terminate with periods.

probname.ver#.out : contains the output from running probname.ver#.in
	with OTTER, with proof if one is found, and with statistics on 
	the clauses generated and CPU time used.


HOW TO RUN :
----------------------------------------------------------------------

Invoke OTTER by using the following command :

	otter < probname.ver#.in    [ > outfile ]   [ & ]

NOTE : '> outfile' may be used to send all output to a file named outfile;
	'&' may be used to run the program in the background.