Tarski Formalization Project: Testing the subformula strategy
The TestSubformulaStrategy program is similar to TestChapter,
except that it generates input files using the subformula strategy. The code for actually
generating the hints that consist of subformulas of the clauses in the NegatedForm
of the theorem is in function InsertSubformulaHintsIntoInputFile in file GenerateInputFiles.php.
The file TestSubformulaStrategy.php is just a short script to control the generation theorem-by-theorem
within a given chapter. Since we want to run each file a long time, this script is good for overnight experiments;
or one can set one theorem's entry in FinalResults to false temporarily to cause an input
file for that theorem to be generated and tested.
We kept the input files and proofs for use with the subformula strategy in separate directories from those
generated without the subformula strategy, to facilitate keeping proofs with hints as well as proofs with the
subformula strategy for the same theorem.
