Michael Beeson's Research

Utility Link | Utility Link | Utility Link

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.