×

Representation and automated transformation of geometric statements. (English) Zbl 1314.68301

Summary: The emergence of a large quantity of digital resources in geometry, various geometric automated theorem proving systems, and kinds of dynamic geometry software systems has made geometric computation, reasoning, drawing, and knowledge management dynamic, automatic or interactive on computer. Integration of electronic contents and different systems is desired to enhance their accessibility and exploitability. This paper proposes an equivalent transformation framework for manipulating geometric statements available in the literature by using geometry software systems. Such a framework works based on a newly designed geometry description language (GDL), in which geometric statements can be represented naturally and easily. The author discusses and presents key procedures of automatically transforming GDL statements into target system-native representations for manipulation. The author also demonstrates the framework by illustrating equivalent transformation processes and interfaces for compiling the transformation results into executable formats that can be interpreted by the target geometry software systems for automated theorem proving and dynamic diagram drawing.

MSC:

68T30 Knowledge representation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
Full Text: DOI

References:

[1] Wu W, Basic principles of mechanical theorem proving in elementary geometries, Journal of Systems Science and Mathematical Sciences, 1984, 4(3): 207-235.
[2] Chou, S.; Gao, X., Automated reasoning in geometry (2001), North Holland · Zbl 1011.68128
[3] List of Interactive Geometry Software, http://en.wikipedia.org/wiki/List of interactive geometry software.
[4] Chen, X.; Wang, D.; Botana, F. (ed.); Recio, T. (ed.), Towards an electronic geometry textbook, No. 4869 (2006)
[5] Chen, X.; Autexier, S. (ed.); Calmet, J. (ed.); Delahaye, D. (ed.); Ion, P. (ed.); Rideau, L. (ed.); Rioboo, R. (ed.); Sexton, A. (ed.), Electronic geometry textbook: A geometric textbook knowledge management system, No. 6167 (2010) · Zbl 1286.68425
[6] Chen X and Wang D, Management of geometric knowledge in textbooks, Data & Knowledge Engineering, 2012, 73: 43-57. · doi:10.1016/j.datak.2011.10.004
[7] Quaresma, P.; Janicić, P.; Tomasevic, J.; Vujosevic-Janicic, M.; Tosic, D., XML-based format for geometry — XML-based format for descriptions of geometrical constructions and geometrical proofs (2008), Ltd. Wellesley, MA, USA
[8] GCLC, http://poincare.matf.bg.ac.rs/janicic//gclc/.
[9] Janicić, P.; Iglesias, A. (ed.); Takayama, N. (ed.), GCLC — A tool for constructive euclidean geometry and more than that, No. 4151 (2006) · Zbl 1230.51024
[10] Janicić P, Geometry constructions language, Journal of Automated Reasoning, 2010, 44(1-2): 3-24. · Zbl 1185.68626 · doi:10.1007/s10817-009-9135-8
[11] GeoThms, http://hilbert.mat.uc.pt/geothms/.
[12] Quaresma P and Janicić P, Geothms — A web system for Euclidean constructive geometry, Electronic Notes in Theoretical Computer Science, 2007, 174(2): 35-48. · Zbl 1278.68279 · doi:10.1016/j.entcs.2006.09.020
[13] Janicić, P.; Quaresma, P.; Furbach, U. (ed.); Shankar, N. (ed.), System description: GCLCprover + Geothms, No. 4130 (2006)
[14] Egido S, Hendriks M, Kreis Y, Kortenkamp U, and Marquès D, i2g Common File Format Final Version, Technical Report D3.10, The Intergeo Consortium, 2010.
[15] Dynamic Geometry Software Speaking I2geo, http://i2geo.net/xwiki/bin/view/Softwares/. · Zbl 1185.68626
[16] Intergeo, http://i2geo.net/. · Zbl 1166.68367
[17] OpenMath, http://www.openmath.org/cd/. · Zbl 1151.68669
[18] TGTP, http://hilbert.mat.uc.pt/TGTP/.
[19] Quaresma, P.; Schreck, P. (ed.); Narboux, J. (ed.); Richter-Gebert, J. (ed.), Thousands of Geometric problems for geometric Theorem Provers (TGTP), No. 6877 (2010)
[20] Chou S, Mechanical Geometry Theorem Proving, Reidel, Dordrecht, 1988. · Zbl 0661.14037
[21] GeoGebra, http://www.geogebra.org/cms/. · Zbl 06671038
[22] GEOTHER, http://www-calfor.lip6.fr/wang/GEOTHER/. · Zbl 1412.68266
[23] Coxeter H S M and Greitzer S L, Geometry Revisited, The Mathematical Association of America, Washington DC, 1967. · Zbl 0166.16402
[24] Cinderella, http://www.cinderella.de/.
[25] Gräbe, H. G.; Winkler, F. (ed.), The symbolicData GEO records — A public repository of geometry theorem proof schemes, No. 2930 (2002) · Zbl 1202.68379
[26] GeoProver, http://www.reduce-algebra.com/docs/geoprover.html. · Zbl 1011.68128
[27] Wang, D.; Winkler, F. (ed.), GEOTHER 1.1: Handling and proving geometric theorems automatically, No. 2930 (2002) · Zbl 1202.68390
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.