Core Library: Proving Theorems

# Proving Geometric Theorems about Ruler-and-Compass Constructions

We introduce a new approach to proving classical theorems about ruler-and-compass constructions. Our approach is a randomized one -- by testing the conjecture on randomly generating instances of a ruler-and-compass construction.

Our prover is based on a generalization of the Schwartz-Zippel Lemma about the randomized zero testing for polynomials. Basically, we generalize the lemma for radical expressions (which also has division and square roots). This result has independent interest.

A version of this prover is in the Core Library distribution (version 1.2 onwards). But we hope to distribute a more full-scale version (with GUI interface, etc) at this website in the future. For technical details, see our paper Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving, by D. Tulone, C. Yap and C. Li, in Proc. Int'l Workshop on Automated Deduction in Geometry (ADG'00), Zurich, Sep 25-27, 2000. The full version can also be found in LNCS/LNAI 2061.

### Evaluation of our Prover

Geometric theorem proving is an active area of research. There are three general approaches: (1) Groebner bases, (2) Wu's Method, and (3) Cell decomposition. Method (1) is very general, but its worst case time is double-exponential. Method (2) proves theorems in complex geometry (or geometry based on any algebraically closed field) and in the worst case is only single-exponential in complexity. Method (3) is a universal method for real geometry, and despite considerable theoretical advances in the 1990's, it remains slow in practice. Our approach is restricted to only ruler-and-compass theorems, and is based on randomization. It is closely related to J.W. Hong's ``proving by example''. Our method has the potential to be one of the fastest methods for this class of theorems for two reasons: (a) it is based on random testing, and (b) radical expressions which is precisely the class of algebraic expressions needed in ruler-and-compass theorems. Our current implementation is straighforward application of the Core Library, and not optimized. For non-linear theorems, we are considerably slower than S.C.Chou's implementation of Wu's method (but, as we said, Wu's method is really about complex geometry). For real geometry, our method is the fastest for this class of theorems. Another interesting property: our method can quickly reject false theorems (rejection of theorems has no error in our method). This property is not available in methods based on (2) or (3). This property is useful in practice, where a researcher may want to test many conjectures, and quickly reject false ones. 