Tarski Formalization Project: Testing the subformula strategy
TestSubformulaStrategy program is similar to
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
of the theorem is in function
InsertSubformulaHintsIntoInputFile in 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
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.