## Tarski Formalization Project: StrategiesWe found proofs of all the approximately 200 theorems that we attempted. These proofs fell into the following categories: - Some were found by OTTER without any special strategy, just using standard values for OTTER parameters like
`max_weight` ,`max_distinct_variables` , etc. Most of these were found in a few minutes, although a few took closer to an hour. - Some theorems were found using the
*diagram strategy*. That refers to defining one (or a few) terms corresponding to the construction of certain points, usually indicated in a geometrical diagram in the book. Such proofs do not rely on the steps of the book proof; they are found without further use of the book proof, once the diagram is given. - Proofs found by the
*subformula strategy*also do not rely on the book proof. Since we used this strategy mainly on difficult theorems, we usually used the diagram too. - When we could not find a proof without reference to the steps of the book proof, we put (at least some of) those
steps in as intermediate goals; that is, in
`list(passive)` ). We used lemma adjunction and hint injection, and often case elimination, to get a proof "by hook or by crook". (All these terms are explained below and in our paper.) When iteration of this process finally produced a proof, we kept the steps as hints, so that the proof can be quickly reproduced.
## The diagram strategy The diagram strategy works because
the defined point is denoted by a single letter instead of a term using, for example, 8 symbols, so the "weight" of such
clauses is smaller by 7, making them less likely to be discarded as exceeding ## The subformula strategy The subformula strategy is very simple: just include as hints
all subformulas of the formulas in the theorem one is trying to prove. By "include a clause as hints", we mean
to place that clause in We had several spectacular successes with the subformula strategy, described on other pages of this website.
Most of the spectacular successes required more than a few minutes to find the proof. To achieve these successes,
we set ## Lemma adjunction and hint injection
After giving up on finding a proof without using the book proof, our next step was to put the (important)
steps of the book proof into
At that point we turned to ## Case elimination
As explained above, we often ended up with a proof of some desired theorem $A$ from a hypothesis $Q$, and
another proof of $A$ from $\neg Q$, but even with both proofs inserted as hints, a proof of $A$ was not
forthcoming. In that case sometimes we could succeed by including the tautology |