TY - GEN
T1 - Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method
AU - McPhee, Nicholas Freitag
AU - Chou, Shang Ching
AU - Gao, Xiao Shan
PY - 1994
Y1 - 1994
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84947917880&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84947917880&partnerID=8YFLogxK
U2 - 10.1007/3-540-58156-1_28
DO - 10.1007/3-540-58156-1_28
M3 - Conference contribution
AN - SCOPUS:84947917880
SN - 9783540581567
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 401
EP - 415
BT - Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings
A2 - Bundy, Alan
PB - Springer Verlag
T2 - 12th International Conference on Automated Deduction, CADE-12 1994
Y2 - 26 June 1994 through 1 July 1994
ER -