Michael Beeson's Research

Tarski Formalization Project: how TestChapter uses previous results

In repeatedly testing our code for the master list and the mechanical generation of input files, we needed a way to specify the way the input files are to be constructed on a per-file basis. To satisfy this need, the file FinalResults.php defines an array FinalResults. This array is used by TestChapter to generate the input files one chapter at a time.

FinalResults is an "associative array", meaning it is indexed not by integers but by the names of theorems. Here is a part of its definition:

    'Satz9.2' =>  10,    
	'Satz9.3a' =>  array(25, "subformula", 46),  // array(25, "hints"),  // 27 steps
	'Satz9.3' =>   array(50, "hints"),   // 52 steps 
	'SideReflect' => array(26, "subformula", 49), //  array(26, "hints"),  //52 steps  
	'Satz9.4a' => array(40, "hints"),  
	'Satz9.4a2' => array(35, "hints"),  // 35 steps
	'Satz9.4b' => array(42,"hints"),  // 48 steps
	'Satz9.4' =>  array(9, "max_weight = 9", "max_seconds = 450"),   // 350 seconds
	'Satz9.4c' => array(41, "hints"),   // 48 steps
	'Satz9.5' => array(30, "subformula",820), // array(12, "hints"),    // 38 steps
	'Satz9.6' => array(98, "subformula", 186), // array(91, "hints"),    // 111 steps
	'Satz9.8' => array(63, "subformula", 1646), //array(48, "hints"),    // 52 steps
	'Satz9.9' => array(6, "max_weight = 8", "max_seconds = 4000"),     
	'Satz9.13' => array(65, "hints"),   
	'Satz9.16' => array(14, "max_weight = 5"), // 7 seconds 
	'Satz9.19b' => array(8, "max_weight = 7"), //  11 seconds        

The first line records the fact that Satz 9.2 can be proved without hints or diagram in 10 steps. The second line says that Satz 9.3a was proved in 25 steps by the subformula strategey, and 46 seconds is more than enough time to find the proof. The third line says that Satz 9.3 was proved in 50 steps using hints. Usually when hints are used, 20 seconds is enough to find the proof; if not then a value of max_seconds is also specified. The entry for Satz 9.9 shows that it could be proved without hints or diagram, but finding that proof required setting a low max_weight and waiting about an hour. (The time shown is a generous value for max_seconds, not the actual time required. Setting max_seconds too large is harmless, as the prover will terminate when it finds the proof.) TestChapter ignores theorems that are listed as being proved by the subformula property. Some theorems can be proved with hints, or without hints using the subformula property. We kept the resulting proofs and input files in different directories. We used a separate program TestSubformulaProperty to attempt to prove theorems by the subformula property. Many of these proofs took more than an hour to find, so having TestChapter attempt to regenerate them would have introduced unacceptable delays. TestChapter runs a whole chapter while you go to get a cup of coffee.