Abstract
The evolution and development of geometry theorem-proving, dating from Euclid’s “Elements” in 3c B.C., may be divided into several stages as indicated in the title of the paper. Achievements in recent years due to the Mathematics-Mechanization Group of the Institute of Systems Science, Academia Sinica are also briefly described.
The present paper is the completed version of a talk given in Learning and Geometry Workshop, Jan. 8–11, 1991, organized by University of Maryland at College Park (UMCP). The author would like to express his warm gratitude to Systems Research Center of UMCP in inviting him for one-month stay and in offering him an agreeable environment to complete his work. The author would like also to express his warm thanks to Ms Cheri Helms for her nice typing of the paper
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bledsoe, W. W. & Loveland, D. W. (eds), Automated theorem proving: after 25 years, Amer. Mathematics Society (1984).
Chou, S. C., Mechanical geometry theorem proving, Reidel (1988).
Chang, C. L. & Lee, C.T., Symbolic Logic and Mechanical theorem Proving, Acad. Press (1973)
Descartes, R., La géomtrie, Paris (1637).
Euclid, Elements, 3c B.C.
Gauss, K. F., Bestimmung der grössten Ellipse walche die vier Seiten einen gegebenen Vierecks berührt in Werke, Bd 4 (1882) 385–392.
Hilbert, D., Grundlagen der Geometrie, (1899).
Ritt, J. F., Differential equations from the algebraic standpoint, Amer. Math. Soc. (1932).
Ritt, J. F., Differential algebra, Amer. Math. Soc. (1950).
Tarski, A., A decision method for elementary algebra and geometry, Berkeley (1950).
Wang, D. M. & Gao, X.S., Geometry theorems proved mechanically using Wu’s method, Math-Mech. Res. Preprints, Inst. Systems Science, No. 2 (1987) 75–105.
Wu Wen-tsün, On the decision problem and the mechanization of theorems in elementary geometry, Scientia Sinica 21(1978) 159–172, Re-publication in [B-L], 213–234.
Wu Wen-tsün, Toward mechanization of geometry-some comments on Hilbert’s “Grundlagen der Geometrie”, Acta Math. Scientia, 2 (1982) 125–188
Wu Wen-tsün, Some remarks on mechanical theorem proving in elementary geometry, Acta Math. Scientia, 3 (1983) 357–360.
Wu Wen-tsün, Basic principles of mechanical theorem proving in geometries. J. Sys. Sci. Math. Scis., 4(1984)207–235. Republished in J. Automated Reasoning, 2 (1986) 221–252.
Wu Wen-tsün, Basic principles of mechanical theorem proving in geometries (Part of elementary geometries), Science Press, Beijing (1984) (in Chinese).
Wu Wen-tsün, On reducibility problems in mechanical theorem proving of elementary geometries, Ch. Quart. J. Math., 2 (1989) 1–20, or Math.-Mech. Res. Preprints, Inst. Sys. Sci., No. 2 (1989) 18–36.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Birkhäuser Boston
About this chapter
Cite this chapter
Wen-Tsün, W. (1996). Geometry Theorem Proving in Euclidean, Descartesian, Hilbertian and Computerwise Fashion. In: Kueker, D.W., Smith, C.H. (eds) Learning and Geometry: Computational Approaches. Progress in Computer Science and Applied Logic, vol 14. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-4088-4_8
Download citation
DOI: https://doi.org/10.1007/978-1-4612-4088-4_8
Publisher Name: Birkhäuser Boston
Print ISBN: 978-1-4612-8646-2
Online ISBN: 978-1-4612-4088-4
eBook Packages: Springer Book Archive