Wu’s method has been shown to be extremely successful in quickly proving large numbers of geomelxy theorems. However, it is not generally complete for real geomeu’y 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 paper 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. A proof of Pompeiu’s theorem using this combination is given, as well as a list of several other challenging theorems proved using this combination.
|Original language||English (US)|
|Title of host publication||Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings|
|Number of pages||15|
|State||Published - 1994|
|Event||12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, France|
Duration: Jun 26 1994 → Jul 1 1994
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||12th International Conference on Automated Deduction, CADE-12 1994|
|Period||6/26/94 → 7/1/94|
Bibliographical noteFunding Information:
*** Chou and Geo were supported in part by NSF Grant CCR-9117870.
Chou and Geo were supported in part by NSF Grant CCR-9117870.
© Springer-Verlag Berlin Heidelberg 1994.