Abstract
In this chapter we will present, for the novice, an introduction to the automated discovery of theorems in elementary geometry. Here the emphasis is on the rationale behind different possible formulations of goals for discovery.
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
Notes
- 1.
Visit https://lsiit-cnrs.unistra.fr/adg2010/index.php/Main_Page for information about the ADG-2010 conference, with links to the URLs of previous meetings.
- 2.
To be considered over a suitable field. There will be different interpretations for different choices of this field. Here we will assume to be in the algebraically closed case, so we will miss, for instance, oriented geometry.
- 3.
For instance, the constructible set (V (R′ 1) ∖ V (R′ 1)) ∪V (R′ 2), where V (R′ 1) = a plane, V (R′ 1) = a line on the plane, V (R′ 2) = a point on this line, can not be expressed as V (R′ 3) ∖ V (R′ 3), for whatever sets of polynomials R′ 3, R′ 3.
References
Bazzotti, L., Dalzotto, G., Robbiano, L.: Remarks on geometric theorem proving”, in automated deduction in geometry (Zurich, 2000), Lecture Notes in Computer Science 2061, 104–128, Springer, Berlin (2001)
Beltrán, C., Dalzotto, G., Recio, T.: The moment of truth in automatic theorem proving in elementary geometry, in Proceedings ADG 2006 (extended abstracts). Botana, F., Roanes-Lozano, E. (eds.) Universidad de Vigo (2006)
Botana, F., Recio, T.: Towards solving the dynamic geometry bottleneck via a symbolic approach in Proceedings ADG (Automatic Deduction in Geometry) 2004. Springer. Lec. Not. Artificial Intelligence LNAI 3763, pp. 761–771 (2005)
Botana, F.: Bringing more intelligence to dynamic geometry by using symbolic computation, in Symbolic Computation and Education. Edited by Shangzhi. L., Dongming, W., Jing-Zhong, Z. World Scientific, pp. 136–150 (2007)
Bulmer, M., Fearnley-Sander, D., Stokes, T.: The Kinds of Truth of Geometric Theorems, in Automated Deduction in Geometry (Zurich, 2000), Lecture Notes in Computer Science 2061, 129–142, Springer, Berlin (2001)
Chen, X.F., Li, P., Lin, L., Wang, D.K.: Proving Geometric Theorems by Partitioned -Parametric Groebner Bases, Automated Deduction in Geometry, LNAI 3763, 34–43, Springer, Berlin (2006)
Chou, S.-C.: Mechanical Geometry Theorem Proving, in Mathematics and its Applications, D. Reidel Publ. Comp. (1987)
Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: the Maclane 83 theorem, in Applied Algebra, Algebraic Algorithms and Error-Correcting Codes (Paris, 1995), Lecture Notes in Computer Science, 948, 183–193, Springer, Berlin (1995)
Conti, P., Traverso, C.: Algebraic and Semialgebraic Proofs: Methods and Paradoxes, in Automated deduction in geometry (Zurich, 2000), Lecture Notes in Comput. Sci. 2061, 83–103, Springer, Berlin (2001)
Dalzotto, G., Recio, T.: On Protocols for the Automated Discovery of Theorems in Elementary Geometry. J. Autom. Reasoning 43, 203–236 (2009)
Kapur, D.: Wu’s method and its application to perspective viewing. In: Geometric Reasoning. Kapur, D. Mundy, J.L. (eds.) The MIT press, Cambridge, MA (1989)
Losada, R., Recio, T., Valcarce, J.L.: Sobre el descubrimiento automático de diversas generalizaciones del Teorema de Steiner-Lehmus, Boletín de la Sociedad Puig Adam, 82, 53–76 (2009) (in Spanish)
Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Groebner systems, In Botana, F., Recio, T. (eds.) Automated Deduction in Geometry, LNAI (Lect. Notes Artificial Intelligence) 4869, pp. 113–139, Springer, Berlin (2007)
Pech, P.: Selected topics in geometry with classical vs. computer proving. World Scientific Publishing Company (2007)
Recio, T., Pilar Vélez, M.: Automatic Discovery of Theorems in Elementary Geometry, J. Autom. Reasoning 23, 63–82 (1999)
Recio, T., Botana, F.: Where the truth lies (in automatic theorem proving in elementary geometry), in Proceedings ICCSA (International Conference on Computational Science and its Applications) 2004. Springer. Lec. Not. Com. Sci. 3044, pp. 761–771 (2004)
http://www.mathematik.uni-bielefeld.de/~sillke/PUZZLES/steiner-lehmus
Wang, D.: Elimination practice: software tools and applications, Imperial College Press, London (2004)
Wen-Tsün, W.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21, 159–172 (1978); Also in: Automated theorem proving: After 25 years (Bledsoe, W. W., Loveland, D. W., eds.), AMS, Providence, pp. 213–234 (1984)
Zeliberger, D.: Plane geometry: an elementary textbook by Shalosh B. Ekhad, XIV, (Circa 2050), http://www.math.rutgers.edu/~zeilberg/PG/gt.html
Acknowledgements
First author supported by grant “Algoritmos en Geometría Algebraica de Curvas y Superficies” (MTM2008-04699-C03-03) from the Spanish MICINN. Second author supported by grant “Geometría Algebraica y Analítica Real” (UCM-910444). Thanks also to the Austrian FWF Special Research Program SFB F013 “Numerical and Symbolic Scientific Computing” for the invitation to present this talk and paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag/Wien
About this chapter
Cite this chapter
Recio, T., Vélez, M.P. (2012). An Introduction to Automated Discovery in Geometry through Symbolic Computation. In: Langer, U., Paule, P. (eds) Numerical and Symbolic Scientific Computing. Texts & Monographs in Symbolic Computation. Springer, Vienna. https://doi.org/10.1007/978-3-7091-0794-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-7091-0794-2_12
Published:
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-0793-5
Online ISBN: 978-3-7091-0794-2
eBook Packages: Computer ScienceComputer Science (R0)