problem-set/logic.problems/README
created : 07/15/86
revised : 08/15/88

Contents of 'logic.problems' :
------------------------------

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

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

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

morgan : logic problems in Equivalential Calculus and Relevance Logic,
	submitted by Charles Morgan, Victoria University.

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

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.