Michael Beeson's Research

Utility Link | Utility Link | Utility Link

Tarski Formalization Project

Tarski 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, OTTER proofs of theorems in Tarskian geometry, describing our methods and results in more detail. This paper was presented at IJCAR-2014 in Vienna (in July, 2014). In September, 2015, we completed and submitted a journal paper for the Journal of Automated Reasoning, with a more systematic view of these methods and results, and some noteworthy extensions. Here is the final prepublication version of that 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.)

Link Description
Archive of input files and proofs Leads to an index by chapter, which leads in turn to all the input files and resulting proofs.
About the master list An explanation of the format of the master list
Testing the master list How we attempted to ensure that the master list is completely correct, including the PHP program we used.
Mechanical generation
of input files
Explanations, and the actual PHP program that generates the files.
About our tools Links to the PHP code for our tools and explanations of the programs
Strategies we used In addition to choosing OTTER settings, we also used diagrams, hints, and the subformula strategy.
Hard and Easy Theorems An explanation of the development of geometry from Tarski's axioms, with particular attention to pointing out what is really difficult in this development.
Results A summary of the results we obtained.

To inspect our input files and proofs, follow the link: