Michael Beeson's Research

Utility Link | Utility Link | Utility Link

Tarski Formalization Project: Results

We used OTTER to find proofs of the theorems in Tarskian geometry in the first nine chapters of Szmielew's development in Part I of Metamathematische Methoden in der Geometrie. Those theorems include the four unsolved challenge problems from Quaife's 1992 book, and the verification of Hilbert's axioms. Of the approximately 200 theorems, we proved 57% mechanically and without strategies (except for a good choice of settings), and by the use of the subformula strategy we increased that to 76%. By using lemma adjunction and hint injection, which depend on starting with a book proof, we achieved a 100% success rate. We have discussed the contents of the book, and the definition of "hard", "simple", and "elementary" theorem (in terms of proof length), on this page. Please refer to that page for a discussion of the theorems mentioned by name in the table below. Here is a table showing the hard theorems from the entire book, with the number of steps in the proof(s) that we obtained. A paired number like $(99,921)$ indicates a proof found mechanically using the subformula strategy, of length 99 and found in 921 seconds. The last column gives the number of steps taken explicitly in the book proof. Not counting the lines with a question mark, we have 1900 Otter steps corresponding to 465 book steps, giving a de Bruijn factor (the ratio of the two).

Theorem Description Subformula Strategy Hints Book
Satz 4.2 inner 5-segment theorem 44 13
Satz 5.1 trichotomy 127 70
Satz 6.16b transitivity of Col 46 1?
Satz 7.13 refl. in pt. preserves congruence $(99, 921)$ 72 28
Satz 7.22a Krippenlemma $(108,3189)$ 96 27
Satz 7.25 isosceles triangle has midpoint 113 34
Satz 8.18 Lotsatz (dropped perpendicular) 227 32
Satz 8.21a uniqueness of dropped perp 106 5
Satz 8.22b existence of midpoint 201 42
Satz 8.24a midpoint details 171 42
Satz 8.24b midpoint details 163 42
Satz 9.3 opposite-side ray theorem 52 14
Satz 9.4b $r=s$ case of 9.4 44 7
Satz 9.6 inner Pasch implies outer Pasch $(98,186)$ 91 27
Satz 9.8 opposite, same implies opposite $(63,1646)$ 48 21
Satz 9.13 transitivity of samesideline 71 1?
Satz 10.2a existence of reflection in line 50 23
Satz 10.2b uniqueness of reflection in line ?? 23
Satz 10.10 refl. in line preserves congruence 92 26
Satz 10.12b right triangle theorem (Euclid 4) 100 14
Satz 10.16a triangle construction 57 24?
Satz 10.16b triangle uniqueness 6022
Satz 11.3a angle congruence theorem 43 18
Satz 11.15a Hilbert's angle transport 77 1