×

Automatic deduction in (dynamic) geometry: Loci computation. (English) Zbl 1280.65021

Summary: A symbolic tool based on open source software that provides robust algebraic methods to handle automatic deduction tasks for a dynamic geometry construction is presented. The prototype has been developed as two different worksheets for the open source computer algebra system Sage, corresponding to two different ways of coding a geometric construction, namely with the open source dynamic geometry system GeoGebra or using the common file format for dynamic geometry developed by the Intergeo project. Locus computation algorithms based on automatic deduction techniques are recalled and presented as basic for an efficient treatment of advanced methods in dynamic geometry. Moreover, an algorithm to eliminate extraneous parts in symbolically computed loci is discussed. The algorithm, based on a recent work on the Gröbner cover of parametric systems, identifies degenerate components and extraneous adherence points in loci, both natural byproducts of general polynomial algebraic methods. Several examples are shown in detail.

MSC:

65D18 Numerical aspects of computer graphics, image analysis, and computational geometry
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Gelernter, H., Realization of a geometry-theorem proving machine, (Feigenbaum, E.; Feldman, J., Computers and Thought, (1963), McGraw-Hill New York), 134-152
[2] Wu, W. T., Mechanical theorem proving in geometries, (1994), Springer Vienna
[3] Wu, W., Some recent advances in mechanical theorem proving of geometries, (Bledsoe, W. W.; Loveland, D. W., Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, (1984), AMS), 235-241
[4] Wu, W., Basic principles of mechanical theorem proving in geometries, Journal of Automated Reasoning, 2, 221-252, (1986) · Zbl 0642.68163
[5] Wang, D.; Gao, X. S., Geometry theorems proved mechanically using wuʼs method - part on Euclidean geometry, MM Research Preprints, 2, 75-106, (1987)
[6] Chou, S. C., Mechanical geometry theorem proving, (1988), D. Reidel Publishing Company Dordrecht, Netherlands · Zbl 0661.14037
[7] Buchberger, B., Gröbner bases: an algorithmic method in polynomial ideal theory, (Bose, N. K., Multidimensional Systems Theory, (1985), Reidel Dordrecht, Netherlands), 184-232 · Zbl 0587.13009
[8] Kapur, D., Geometry theorem proving using hilbertʼs nullstellensatz, (Char, B. W., SYMSACʼ86: Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation, (1986), ACM Press New York, NY, USA), 202-208
[9] Chou, S. C.; Schelter, W. F., Proving geometry theorems with rewrite rules, Journal of Automated Reasoning, 2, 253-273, (1986) · Zbl 0642.68162
[10] Kutzler, B.; Stifter, S., Automated geometry theorem proving using buchbergerʼs algorithm, (Char, B. W., SYMSACʼ86: Proceedings of the Fifth ACM Symposium on Symbolic and Algebraic Computation, (1986), ACM Press New York, NY, USA), 209-214 · Zbl 0629.68086
[11] Kapur, D.; Mundy, J. L., Wuʼs method and its application to perspective viewing, Artificial Intelligence, 37, 15-26, (1988) · Zbl 0664.68102
[12] Recio, T.; Vélez, M. P., Automatic discovery of theorems in elementary geometry, Journal of Automated Reasoning, 23, 63-82, (1999) · Zbl 0941.03010
[13] X.S. Gao, J.Z. Zhang, S.C. Chou, Geometry Expert, Nine Chapters, Taiwan, 1998.
[14] Wang, D., Geother: A geometry theorem prover, (McRobbie, M. A.; Slaney, J. K., Automated Deduction - Cade-13, Lectures Notes in Computer Science, vol. 1104, (1996), Springer), 166-170 · Zbl 1412.68266
[15] Botana, F.; Valcarce, J. L., A dynamic-symbolic interface for geometric theorem discovery, Computers and Education, 38, 21-35, (2002)
[16] Roanes-Lozano, E.; Roanes-Macías, E.; Villar, M., A bridge between dynamic geometry and computer algebra, Mathematical and Computer Modelling, 37, 1005-1028, (2003) · Zbl 1073.68899
[17] Escribano, J.; Botana, F.; Abánades, M. A., Adding remote computational capabilities to dynamic geometry systems, Mathematics and Computers in Simulation, 80, 1177-1184, (2010)
[18] Montes, A.; Wibmer, M., Gröbner bases for polynomial systems with parameters, Journal of Symbolic Computation, 45, 1391-1425, (2010) · Zbl 1207.13018
[19] Dewar, M., Openmath: an overview, ACM SIGSAM Bulletin, 34, 2, 2-5, (2000)
[20] Botana, F., Interactive versus symbolic approaches to plane loci generation in dynamic geometry environments, (Sloot, P. M.; Hoekstra, A.; Tan, C. K.; Dongarra, J. J., Computational Science - ICCS 2002, Lecture Notes in Computer Science, vol. 2330, (2002), Springer Berlin, Heidelberg), 211-218 · Zbl 1055.68580
[21] Lebmeir, P.; Richter-Gebert, J., Recognition of computationally constructed loci, (Botana, F.; Recio, T., Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 4869, (2007), Springer Berlin, Heidelberg), 52-67 · Zbl 1195.68105
[22] Gerhäuser, M.; Wassermann, A., Automatic calculation of plane loci using Gröbner bases and integration into a dynamic geometry system, (Schreck, P.; Narboux, J.; Richter-Gebert, J., Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877, (2011), Springer Berlin, Heidelberg), 68-77 · Zbl 1350.68295
[23] Chou, S. C., Proving elementary geometry theorems using wuʼs algorithm, (Bledsoe, W. W.; Loveland, D. W., Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, (1984), American Mathematical Society), 243-286
[24] Roanes-Macías, E.; Roanes-Lozano, E., Automatic determination of geometric loci. 3d-extension of Simson-Steiner theorem, (Campbell, J. A.; Roanes-Lozano, E., Artificial Intelligence and Symbolic Computation, Lecture Notes in Computer Science, vol. 1930, (2001), Springer Berlin, Heidelberg), 157-173 · Zbl 1042.68129
[25] Kapur, D., Using Gröbner bases to reason about geometry problems, Journal of Symbolic Computation, 2, 4, 399-408, (1986) · Zbl 0629.68087
[26] Winkler, F., Gröbner bases in geometry theorem proving and simplest degeneracy conditions, Mathematica Pannonica, 1, 15-32, (1990) · Zbl 0725.68090
[27] Botana, F., On the parametric representation of dynamic geometry constructions, (Murgante, B.; Gervasi, O.; Iglesias, A.; Taniar, D.; Apduhan, B., Computational Science and Its Applications - ICCSA 2011, Lecture Notes in Computer Science, vol. 6785, (2011), Springer Berlin, Heidelberg), 342-352
[28] Todd, P., Geometry expressions: a constraint based interactive symbolic geometry system, (Botana, F.; Recio, T., Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Lecture Notes in Artificial Intelligence, vol. 4689, (2007), Springer-Verlag Berlin, Heidelberg, New York), 189-202 · Zbl 1195.68116
[29] Virtual box server for automatic deduction, Last accessed January 2013
[30] Sage lite server2, Last accessed January 2013
[31] Caprotti, O.; Cohen, A. M., On the role of openmath in interactive mathematical documents, Journal of Symbolic Computation, 351-364, (2001) · Zbl 0981.68185
[32] Barendregta, H.; Cohen, A. M., Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, Journal of Symbolic Computation, 32, 3-22, (2001) · Zbl 1074.68077
[33] Intergeo, Last accessed January 2013
[34] Jsxgraph, Last accessed January 2013
[35] Botana, F.; Valcarce, J. L., A software tool for the investigation of plane loci, Mathematics and Computers in Simulation, 61, 2, 139-152, (2003) · Zbl 1011.68149
[36] Schauenburg, P., A Gröbner-based treatment of elimination theory for affine varieties, Journal of Symbolic Computation, 42, 859-870, (2007) · Zbl 1137.13018
[37] Recio, T.; Vélez, M. P., An introduction to automated discovery in geometry through symbolic computation, (Langer, U.; Paule, P., Numerical and Symbolic Scientific Computing, Texts and Monographs in Symbolic Computation, vol. 1, (2012), Springer Vienna), 257-271 · Zbl 1250.65040
[38] Weispfenning, V., Comprehensive Gröbner bases, Journal of Symbolic Computation, 14, 1-29, (1992) · Zbl 0784.13013
[39] Suzuki, A.; Sato, Y., An alternative approach to comprehensive Gröbner bases, Journal of Symbolic Computation, 36, 649-667, (2003) · Zbl 1053.13013
[40] Montes, A., A new algorithm for discussing Gröbner basis with parameters, Journal of Symbolic Computation, 33, 183-208, (2002) · Zbl 1068.13016
[41] Lazard, D.; Rouillier, F., Solving parametric polynomial systems, Journal of Symbolic Computation, 42, 636-667, (2007) · Zbl 1156.14044
[42] Kapur, D.; Sun, Y.; Wang, D., A new algorithm for computing comprehensive Gröbner systems, (Watt, S. M., ISSAC ʼ10 Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, (2010), ACM New York), 29-36 · Zbl 1321.68533
[43] Chen, X.; Li, P.; Lin, L.; Wang, D., Proving geometric theorems by partitioned-parametric Gröbner bases, (Hong, H.; Wang, D., Automated Deduction in Geometry, 5th International Workshop, ADG 2004, Lectures Notes on Artificial Intelligence, vol. 3763, (2006)), 34-43 · Zbl 1159.68550
[44] Montes, A.; Recio, T., Automatic discovery of geometry theorems using minimal canonical comprehensive Gröbner systems, (Botana, F.; Recio, T., Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Lecture Notes in Artificial Intelligence, vol. 4689, (2007), Springer-Verlag Berlin, Heidelberg, New York), 113-139 · Zbl 1195.68093
[45] Moreno Maza, M.; Xia, B.; Xiao, R., On solving parametric polynomial systems, Mathematics in Computer Science, 6, 457-473, (2012) · Zbl 1274.13047
[46] Suzuki, A., Last accessed January 2013
[47] Botana, F.; Valcarce, J. L., Automatic determination of envelopes and other derived curves within a graphic environment, Mathematics and Computers in Simulation, 67, 1-2, 3-13, (2004) · Zbl 1091.68111
[48] Suzuki, A.; Sato, Y., A simple algorithm to compute comprehensive Gröbner bases using Gröbner bases, (Proceedings of the 2006 International Symposium on Symbolic and Algebraic Computation, ISSAC ʼ06, (2006), ACM New York, NY, USA), 326-331 · Zbl 1356.13040
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.