problem-set

Click here to see the number of accesses to this library.


# 
#  ====== index for problem-set ======
# 
#  problem-set/README
#  created : 06/30/88
#  revised : 08/15/88
#  
#  Contents of 'problem-set' :
#  ---------------------------
#  
#  NOTE : This database is formatted into several directories and each of
#  those into subdirectories, grouped by the type of problem treated.  There
#  are separate directories for areas of mathematics, puzzles, and other uses
#  of automated reasoning programs.  Here is a brief list of the
#  subdirectories :
#   
#  Main Directory Headings
#  ----------------------------------------------------------------------
#  

lib	algebra
for	algebra : algebra problems in the fields of boolean algebras, category 
,  	theory, group theory, henkin models, modular lattices, and ring 
,  	theory.	

lib	analysis
for	analysis : analysis problems in the field of limit theorems.

lib	circuits
for	jcircuits : circuit design and validation problems.

lib	geometry
for	geometry : geometry problems in the field of tarskian geometry.

lib	logic.problems
for	logic.problems : logic problems in Equivalential Calculus and Relevance
,	logic.

lib	miscellany
for	miscellany : miscellaneous problems.

lib	pelletier
for	pelletier : problems submitted by Francis Pelletier, from "75 Problems for 
,	Testing ITP".

lib	prog.verification
for	prog.verification : problems in program verification.

lib	puzzles
for	puzzles : puzzles formulated for the theorem prover to solve.

lib	set.theory
for	set.theory : set theory problems using naive set theory and Godel's axioms.

lib	topology
for	topology : topology problems. 


#  ----------------------------------------------------------------------
#  
#  Inside each of the above subdirectories, you will find several files:
#  
#  1) a README file, similar in format to this one, giving short explanations
#  	of what the problems are about;
#  
#  2) .desc files, which are slightly longer English descriptions of the
#  	problems, and credits for their creation;
#  
#  3) .clauses files, which are the commentary and clauses for the problems;
#  
#  4) .in files, which are OTTER input files, with inference rules specified;
#  
#  5) .out files, which are actual OTTER output.
#  
#  Note that there may be several versions of each problem, which may differ
#  only in inference rules used, or may have different axioms or a different
#  choice of the set of support.  Also, the date which appears at the top of
#  the .out files is the version date of OTTER which was used to produce that
#  output file.
#  
#  ----------------------------------------------------------------------
#  
#  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.
#