## 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:
Here `$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
The heart of this program is ` 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 It will be easy to modify |