Abstract
Wu's method has been shown to be extremely 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 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.
Chou and Gao were supported in part by NSF Grant CCR-9117870.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
D. S. Arnon. Geometric reasoning with logic and algebra. Artificial Intelligence Journal, 37:37–60, 1988.
S. C. Chou. Proving and discovering theorems in elementary geometries using Wu's method. PhD thesis, Department of Mathematics, University of Texas, Austin, 1985.
S. C. Chou. Mechanical geometry theorem proving. D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.
S. C. Chou and X. S. Gao. Ritt-Wu's decomposition algorithm and geometry theorem proving. In M. E. Stickel, editor, Proceedings of the 10th international conference on automated deduction. Springer-Verlag, 1990.
S. C. Chou and X. S. Gao. Techniques for Ritt-Wu's decomposition algorithm. In Proceedings of the IWMM. International Academic Publishing, 1992.
S. C. Chou, X. S. Gao, and D. S. Arnon. On the mechanical proof of geometry theorems involving inequalities. Technical Report TR-89-31, Department of Computer Sciences, University of Texas at Austin, October 1989.
S. C. Chou, X. S. Gao, and N. F. McPhee. A combination of Ritt-Wu's method and Collins' method. Technical Report TR-89-28, Department of Computer Sciences, University of Texas at Austin, October 1989.
G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceeding Second GI Conference on Automata Theory and Formal Languages, volume 33 of Lecture Notes In Computer Science, pages 134–183. Springer-Verlag, 1975.
Hoon Hong. Improvements in CAD-based quantifier elimination. PhD thesis, Computer and Information Science Research Center, The Ohio State University, 1990. Technical Report OSU-CISRC-10/90-TR29.
Nicholas Freitag McPhee. Mechanically proving geometry theorems using Wu's method and Collins' method. PhD thesis, University of Texas at Austin, 1993.
Wu Wen-tsün. Basic principles of mechanical theorem proving in geometries. J. of Sys. Sci. and Math. Sci., 4(3):207–235, 1984. Republished in Journal of Automated Reasoning, 2(4):221–252, 1986.
Wu Wen-tsün. On zeros of algebraic equations — an application of Ritt's principle. Kexue Tongbao, 31(1):1–5, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McPhee, N.F., Chou, SC., Gao, XS. (1994). Mechanically proving geometry theorems using a combination of Wu's method and Collins' method. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_28
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive