Mechanical Generation of Input Files
Once the master list is correct, it is a routine programming exercise
involving only textual (string) manipulations to generate input files.
The algorithm is simple. Consider, for example, the function
with the specification given in the following comments:
function InputFileAsArray($t, $diagrams, $sos, $settings, $cases)
// $t should be a member of $TarskiTheorems
// Generate the lines of an input file for proving $t
// and return an array of strings containing those lines.
// Make sure no line exceeds 80 characters.
// include the diagram if $diagrams is not false.
// include the members of $t->Cases if it is an array
$settings is an array of the OTTER settings to be used
in this file; the strings in the arrays
$t->Diagrams, $t->NegatedForm, and $t->Cases
are ready to be copied out of $t into the appropriate places in a file
template. All the function has to do is
create an array $ans and add these things to that array in the right
order, interspersing template lines like list(sos). at the appropriate places.
This function, however, doesn't put any hints into the file it is creating.
That is done by
function InsertHintsIntoInputFile($theorem_name, $outdir, $indir)
// Get hints from the proof, i.e. from the .prf file
// found in directory $outdir, and insert them in
// list(hints) in the input file.
GetHintsFromProof, which we have been
using since 2012 to extract hints by hand from a proof; we have confidence
in the correctness of that program based on long use and on many comparisons
of the output with the input. Again, the correctness of that program doesn't
really matter, since whatever we put into the hints list, if we get a proof,
the proof is right. To ensure correctness of any proofs obtained,
the only thing that really matters about InsertHintsIntoInputFile
is that all it does to the input file is add a hints list. (Of course,
to actually obtain some proofs, it had better be correct in other ways.)
An important point about correctness is that
it does not matter what is in the hints list. If you get a proof,
it is a proof, regardless of what was in the hints list. In our mechanical generation
of input files, we make use of the (possibly unreliable) proofs we found in 2012.
If we cannot find a proof without hints, then we use the steps of an existing (alleged)
proof as hints.
As our testing progressed, we wanted to run OTTER on all the theorems of a given chapter
in the book, using the settings that we found best for each theorem in previous runs.
That is, some theorems required a diagram, but not hints, and some required hints, and
later on, we were able to prove some of those without hints using the subformula strategy.
To generate these different input files mechanically, we used another program TestChapter
in conjunction with the functions described on this page. It is described here.
It will be easy to modify GenerateInputFiles to produce input files for
other theorem provers or proof checkers. This opens the door to easy experimentation for
those who want to compare the performance of different provers on this body of theorems.
