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 perfile basis. To satisfy this need, the file
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.
