Tarski Formalization Project: TestChapter
The TestChapter program arose out of the desire to test
our formal development on all the theorems of a given chapter by issuing
one command. We wanted to do that for these reasons:
- To regenerate all the proofs after a change in the Master List
- To see the effect of a change in settings. For example, could we still
prove all the theorems of this chapter with a lower value of
max_variables?
However, the different theorems require differently constructed input files:
- Without diagram or hints
- With diagram but without hints
- With both diagram and hints
- Using the subformula strategy (but not hints)
- Some files required a large value of
max_seconds or a smaller or larger value of max_weight.
We therefore kept a machine-readable (but handwritten) record of our results so far, in
FinalResults.php.
This file is consulted by
TestChapter and the input files are constructed accordingly.
An explanation of
FinalResults can be found
here.
