Automated development of Tarski's geometry

Tarski's geometry, a complete first-order axiomatization of Euclidean plane geometry, is developed within the automated reasoning system OTTER. Proofs are obtained and performance statistics supplied for most of the challenge problems appearing in the literature. Few of these problems have been previously solved by any clause-based reasoning system. Further challenges are offered.