problem-set/analysis/limits/README created : 07/21/86 revised : 07/20/88 Contents of 'limits' : ---------------------- NOTE : These are problems in limit theorems, which were obtained from W.W. Bledsoe through a private correspondance. No natural language descriptions are available. Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/analysis/limits. axioms : a strategy-free clause list of the axioms in limit theory, subsets of which are used in the limit theorem problems #1, 2. prob1 : as above. prob2 : as above. ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver# : 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#, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver# through 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# [ > 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.