Michael Beeson's Research

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