Otter proofs in Tarskian geometry

ABSTRACT. We report on a project to use Otter to find proofs of the theorems in Tarskian geometry proved in Szmielew's part (Part I) of the book by Schwabhäuser, Szmielew, and Tarski. These theorems start with fundamental properties of betweenness, and end with the development of geometric definitions of addition and multiplication that permit the representation of models of geometry as planes over Euclidean fields, or over real-closed fields in the case of full continuity. They include the four challenge problems left unsolved by Quaife, who two decades ago found some Otter proofs in Tarskian geometry. Our methodology was to present each theorem to Otter as an isolated problem, giving it the (negated) theorem as a goal, and the previous theorems (and the axioms) to use. In practice, we had to coax Otter a bit more.

Quaife's four challenge problems were: every line segment has a midpoint; every segment is the base of some isosceles triangle; the outer Pasch axiom (assuming inner Pasch as an axiom); and the first outer connectivity property of betweenness. These are to be proved without any parallel axiom and without even line-circle continuity. These are difficult theorems, the first proofs of which were the heart of Gupta's Ph.~D. thesis under Tarski. Otter proved them all in 2012. Our success, we argue, is due to improvements in techniques of automated deduction, rather than to increases in computer speed and memory.

The theory of Hilbert (1899) can be translated into Tarski's language, interpreting lines as pairs of distinct points, and angles as ordered triples of non-collinear points. Under this interpretation, the axioms of Hilbert either occur among, or are easily deduced from, theorems in the first 11 (of 16) chapters of Szmielew. At the time of writing this abstract, we have proved all but the two axioms about angles, III.3 and III.4, and we will finish that soon. Narboux and Braun have recently checked these same proofs in Coq.