Automated development of Tarski's geometry (Q1825046)

The author uses McCune's automated reasoning system to prove theorems in Euclidean plane geometry within the framework of Tarski's axiomatization (this is a first-order axiomatization which was shown by Tarski to be complete and decidable). McCune's automated reasoning system OTTER is a resolution based theorem prover (hyperresolution was used in most cases) but it is not interactive. The author carefully comments about his choice of weight for retained clauses. He proved various ``challenge problems'' on a VAX 8800 and gives performance statistics for the challenge problems. In addition, he comments briefly upon the performance of a CRAY X-MP/14 and poses further challenge problems.