Michael Beeson's Research

Utility Link | Utility Link | Utility Link

Tarski Formalization Project: Tools written in PHP

On this page we provide links to

  • Explanations of the tools we wrote; and
  • Links to the tools themselves.
The tools consist of PHP files. In order that the PHP files be readable right now in your browser, we have renamed them by adding the file extension .txt. For example, MasterList.php has been posted as MasterList.php.txt. That way, the server will not try to execute the code when you click on a link to it, but simply display it for your reading pleasure. If you want to download and use these programs, just save them locally in files without the added extension. The first column of the following table contains links to these text files:

Program Purpose Explanation Page
TarskiTheorems The master list About the Master List
TestMasterList Apply several syntactic tests to check the correctness of the master list. Test the Master List
GenerateInputFiles Use the master list to generate input files. About GenerateInputFiles
TestChapter Run Otter on all the theorems from one chapter with settings taken from previous results. About TestChapter
FinalResults Keep a machine-readable (but handwritten) record of experimental results, for use by TestChapter. About FinalResults
TestSubformulaStrategy Prepare input files and run tests of the subformula strategy. About TestSubformulaStrategy
ExtractProofs Extract proofs from Otter output files. About ExtractProofs