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.