Guide to the proof summary files.

The proof summary files have been automatically extracted from Otter input and output files using a Perl script. The following guide explains briefly what each of the proof summary directories contain.

The directories are listed here in alphabetical order. The logical order in which the theorems could be proved can be determined by examining the standard input file.

Each group contains a text file called all.pos which lists formulas for all the theorems proved in that group. The accompanying file all.cls contains the clauses that Otter generated from these formulas, and Otter's suggestions about which equations could be made into demodulators. Some groups contain a file all.txt that discusses the lex order.

The proof summaries of individual theorems are found in the text files with extension .sum. There may also be files with extension .txt that contain notes concerning the proofs of some theorems.

Input and output files are available by e-mail request.

Link back to main Otter proofs directory.

Last modified: 2002 August 5