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.

Download the prover (April 2001).