Abstract
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 |
| Editors | Alan Bundy |
| Publisher | Springer Verlag |
| Pages | 401-415 |
| Number of pages | 15 |
| ISBN (Print) | 9783540581567 |
| DOIs | |
| State | Published - 1994 |
| Event | 12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, France Duration: Jun 26 1994 → Jul 1 1994 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 814 LNAI |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 12th International Conference on Automated Deduction, CADE-12 1994 |
|---|---|
| Country/Territory | France |
| City | Nancy |
| Period | 6/26/94 → 7/1/94 |
Bibliographical note
Funding Information:*** Chou and Geo were supported in part by NSF Grant CCR-9117870.
Funding Information:
Chou and Geo were supported in part by NSF Grant CCR-9117870.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.