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.