Michael Beeson's Research

Utility Link | Utility Link | Utility Link

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.