Michael Beeson's Research

Utility Link | Utility Link | Utility Link

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
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
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.
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 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.