Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method

Nicholas Freitag McPhee; Shang Ching Chou; Xiao Shan Gao

doi:10.1007/3-540-58156-1_28

Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method

Nicholas Freitag McPhee, Shang Ching Chou, Xiao Shan Gao

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

6 Scopus citations

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	https://doi.org/10.1007/3-540-58156-1_28
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	France
City	Nancy
Period	6/26/94 → 7/1/94

Access

10.1007/3-540-58156-1_28

Fingerprint Dive into the research topics of 'Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method'. Together they form a unique fingerprint.

Cite this

McPhee, N. F., Chou, S. C., & Gao, X. S. (1994). Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method. In A. Bundy (Ed.), Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings (pp. 401-415). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 814 LNAI). Springer Verlag. https://doi.org/10.1007/3-540-58156-1_28

Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method. / McPhee, Nicholas Freitag; Chou, Shang Ching; Gao, Xiao Shan.

Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. ed. / Alan Bundy. Springer Verlag, 1994. p. 401-415 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 814 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

McPhee, NF, Chou, SC & Gao, XS 1994, Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method. in A Bundy (ed.), Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 814 LNAI, Springer Verlag, pp. 401-415, 12th International Conference on Automated Deduction, CADE-12 1994, Nancy, France, 6/26/94. https://doi.org/10.1007/3-540-58156-1_28

McPhee NF, Chou SC, Gao XS. Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method. In Bundy A, editor, Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1994. p. 401-415. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-58156-1_28

McPhee, Nicholas Freitag ; Chou, Shang Ching ; Gao, Xiao Shan. / Mechanically proving geometry theorems using a combination of Wu’s method and Collins’ method. Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. editor / Alan Bundy. Springer Verlag, 1994. pp. 401-415 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8bd26261c3cb4280ba02b45adce481a3,

title = "Mechanically proving geometry theorems using a combination of Wu{\textquoteright}s method and Collins{\textquoteright} method",

abstract = "Wu{\textquoteright}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{\textquoteright}y and is unable to handle inequality problems. Collins{\textquoteright} 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{\textquoteright}s method and the (current) practical reach of Collins{\textquoteright} method. A proof of Pompeiu{\textquoteright}s theorem using this combination is given, as well as a list of several other challenging theorems proved using this combination.",

author = "McPhee, {Nicholas Freitag} and Chou, {Shang Ching} and Gao, {Xiao Shan}",

year = "1994",

doi = "10.1007/3-540-58156-1_28",

language = "English (US)",

isbn = "9783540581567",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "401--415",

editor = "Alan Bundy",

booktitle = "Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings",

note = "12th International Conference on Automated Deduction, CADE-12 1994 ; Conference date: 26-06-1994 Through 01-07-1994",

}

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 -