| Wu's method has been shown to be enormously successful in quickly proving large numbers of geometry theorems. However it is not generally complete for real geometry and is unable to handle inequality problems. Collins' method is complete for real geometry and is able to handle inequality problems, but is not at the moment able to prove some of the more challenging theorems in a practical amount of time and space. This dissertation presents a combination that is capable of proving theorems beyond the theoretical reach of Wu's method and the (current) practical reach of Collins' method, thereby filling one of the few remaining holes in the space of elementary geometry theorems that can be automatically proved. Examples of theorems proved using this combination are given, as well as the proofs generated. These examples include the Steiner-Lehmus theorem, which is listed as a challenge problem in (CGA89), and Pompeiu's theorem.;Also presented is an improved algorithm for Ritt-Wu decomposition, a crucial component in Wu's method and the combination. This new algorithm avoids much of the unnecessary non-determinism in the more traditional algorithm, resulting in significant improvements in performance. |
