## Tarski Formalization ProjectTarski gave a short list of axioms for geometry, which in its final version, consists of only ten axioms A1-A10, plus one or more axioms of continuity A11. A development of Euclidean geometry from this minimal list of axioms, up to and including the geometrical definitions of addition, multiplication, and square root as developed by Descartes and Hilbert, is carried out in the book In 2012, Larry Wos and I undertook to formalize Szmielew's work, using the theorem-prover Otter to produce computer-checkable proofs of each theorem (Satz). There are 16 chapters. In 2012, we obtained Otter proofs of the theorems in the first nine chapters, up to and including Satz 9.6. Highlights of this portion of the work include the major theorems of Gupta's famous 1965 Ph. D. thesis, In February 2013, we returned to this project. We wished to have Otter proofs verifying the axioms of Hilbert's geometry (as expressed in Tarski's language). Many of Hilbert's axioms are included in the first nine chapters, but two of his axioms about angle congruence are in Chapter 11, and his parallel axiom is in Chapter 12. Specifically, we needed to prove Satz 9.9, 11.15, 11.49, and 12.11, and of course, the theorems on which those theorems depend, in particular the difficult Satz 11.4. For a detailed examination of Hilbert's axioms and their interpretation in Tarski's language, and a list of the theorems in SST required to prove Hilbert's axioms, see Proving Hilbert's axioms in Tarski geometry. We wrote a paper,
After the Vienna presentation, we had 214 theorems of geometry, each with its own OTTER file. These files were prepared by hand, with a lot of editing. There were many opportunities for human error (and there were many human errors). We wanted to eliminate the possibility that a human error in manipulating these files could cause bogus proofs; and at the same time, we wanted to be able to run experiments over the whole set of 214 files. Therefore we wished to develop computer programs to mechanically generate our input files and to test them. In particular, each theorem has a Once we decided that we wanted mechanically generated input files, it became clear that we needed a We briefly thought about printing the Master List in an appendix of our paper. However, upon giving that a try, we found that the Master List was 43 pages long at that time--too long to include in a paper. We will make it available on this website, and we may place it on the ArXiv as well (where it should live longer than this website will live). We used the master list to create mechanically generated OTTER input files. On a page linked below, you can find a complete description of how these mechanically generated files are constructed. Some of them use "hints" obtained from the proofs we found in the first phase of this project (or "somehow"--it doesn't matter where the proof came from). Some of them use the "subformula strategy" (also linked below). Some of them just use the "diagram" (also explained on a page linked below). The files themselves are also all available on this website. They all will prove on your machine using OTTER, at least, if you run them one at a time. (Each contains a time limit that is more than sufficient on our current machines.) There is quite a bit to say about the experiments we performed with these input files and the results of
those experiments. Of course, that is the subject of our forthcoming paper in the
To inspect our input files and proofs, follow the link: |