Michael Beeson's Research
-->
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 Metamathematische Methoden in der Geometrie, by W. Schwäbhauser, W. Szmielew, and A. Tarski. (That book as recently been reprinted, with a new foreword). The relevant part of the book is Part I, which is due to Wanda Szmielew, and is based on her 1965 course notes from UC Berkeley. Below and elsewhere on this website, we call this book SST, or just "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, Contributions to the Axiomatic Foundations of Geometry, and the four "challenge problems" left by Art Quaife in his 1992 book, Automated Development of Mathematical Theories. 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 NegatedForm, which is a list of clauses containing the hypotheses and the negated conclusion of the theorem, and also a PositiveForm, which is the clausal form of the theorem that is included in subsequent files, so the theorem can be used to prove other theorems. The positive form is obtained from the negative form by "Skolemization". If there are variables in the NegatedForm (that is, the proof is supposed to show that something exists), then the PositiveForm introduces a new "Skolem function". Originally we performed this Skolemization process by hand. Once we decided that we wanted mechanically generated input files, it became clear that we needed a Master List of all the theorems. Each entry in the master list contains the NegatedForm and the PositiveForm of the theorem, as well as other information about the theorem. We wrote a program TestMasterList to check that the Skolemizations are all correct, and to check everything else that we could think of to check about the Master List. The master list is available on this website (see the links at the bottom of this page). We think that it might possibly be the most useful product of this research, because other researchers will be able to use it for their own purposes (for example, to generate input files for a different prover, or to translate the theorems into the language of their favorite proof checker). 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 Journal of Automated Reasoning. But this website contains some summaries and tables that are not in the paper, as well as possibly being more up to date; and it contains all the computer programs (written in PHP) that we used, along with explanations, neither of which are in the paper. See the links below. (They ones that are not yet live should go live in the next few days; but the original input files have already been replaced by mechanically generated files, and the tables that index these files and their proofs are now dynamically computed from the latest results.)
To inspect our input files and proofs, follow the link: |