×

Automatic verification of regular constructions in dynamic geometry systems. (English) Zbl 1195.68092

Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 39-51 (2007).
Summary: We present an application of automatic theorem proving (ATP) in the verification of constructions made with dynamic geometry software (DGS). Given a specification language for geometric constructions, we can use its processor to deal with syntactic errors. The processor can also detect semantic errors – situations when, for a given concrete set of geometrical objects, a construction is not possible. However, dynamic geometry tools do not test if, for a given set of geometrical objects, a construction is geometrically sound, i.e., if it is possible in a general case. Using ATP, we can do this last step by verifying the geometric constructions deductively. We have developed a system for the automatic verification of regular constructions (made within DGSs GCLC and Eukleides), using our ATP system, GCLCprover. This gives a real-world application of ATP in dynamic geometry tools.
For the entire collection see [Zbl 1132.68006].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51-04 Software, source code, etc. for problems pertaining to geometry
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bertot, Y.; Guilhot, F.; Pottier, L., Visualizing geometrical statements with GeoView, Electr. Notes Theor. Comput. Sci., 103, 49-65 (2004)
[2] Botana, F.; Valcarce, J. L., A dynamic-symbolic interface for geometric theorem discovery, Computers and Education, 38, 21-35 (2002)
[3] Buchberger, B.; Craciun, A.; Jebelean, T.; Kovacs, L.; Kutsia, T.; Nakagawa, K.; Piroi, F.; Popov, N.; Robu, J.; Rosenkranz, M.; Windsteiger, W., Theorema: Towards computer-aided mathematical theory exploration, Journal of Applied Logic, 4, 4, 470-504 (2006) · Zbl 1107.68095
[4] Chou, S.-C.; Gao, X.-S.; Zhang, J.-Z.; Vardi, M., Automated production of traditional proofs for constructive geometry theorems, LICS. Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, 48-56 (1993), Los Alamitos: IEEE Computer Society Press, Los Alamitos
[5] Chou, S.-C.; Gao, X.-S.; Zhang, J.-Z., Automated generation of readable proofs with geometric invariants, I. multiple and shortest proof generation, Journal of Automated Reasoning, 17, 325-347 (1996) · Zbl 0865.68109
[6] Fuchs, K., Hohenwarter, M.: Combination of dynamic geometry, algebra and calculus in the software system geogebra. In: Computer Algebra Systems and Dynamic Geometry Systems in Mathematics Teaching Conference 2004, Pecs, Hungary, pp. 128-133 (2004)
[7] Gao, X.-S.: GEX, http://www.mmrc.iss.ac.cn/ xgao/software.html
[8] Gao, X.-S.; Lin, Q.; Winkler, F., MMP/Geometer - a software package for automated geometric reasoning, Automated Deduction in Geometry, 44-66 (2004), Heidelberg: Springer, Heidelberg · Zbl 1202.68378
[9] Gao, X.S., Lin, Q.: MMP/Geometer, http://www.mmrc.iss.ac.cn/ xgao/software.html
[10] Jackiw, N.: The Geometer’s Sketchpad v4.0. In: Emeryville: Key Curriculum Press (2001)
[11] Janičić, P.; Iglesias, A.; Takayama, N., GCLC — a tool for constructive euclidean geometry and more than that, Mathematical Software - ICMS 2006, 58-73 (2006), Heidelberg: Springer, Heidelberg · Zbl 1230.51024
[12] Janičić, P.; Quaresma, P.; Furbach, U.; Shankar, N., System Description: GCLCprover + GeoThms, Automated Reasoning, 145-150 (2006), Heidelberg: Springer, Heidelberg
[13] Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Procedings of the Mathematical User-Interfaces Workshop 2004 (2004)
[14] Laborde, J. M.; Strässer, R., Cabri-géomètre: A microworld of geometry guided discovery learning, International reviews on mathematical education- Zentralblatt fuer didaktik der mathematik, 90, 5, 171-177 (1990)
[15] Liang, T.; Wang, D.; Hong, H.; Wang, D., Towards a geometric-object-oriented language, Automated Deduction in Geometry, 130-155 (2006), Heidelberg: Springer, Heidelberg · Zbl 1159.68554
[16] Liang, T., Wang, D.: Geometric constraint handling in Gool. In: Automated Deduction in Geometry, pp. 66-73 (2006)
[17] Matsuda, N.; Vanlehn, K., Gramy: A geometry theorem prover capable of construction, Journal of Automated Reasoning, 32, 3-33 (2004)
[18] Narboux, J.; Slind, K.; Bunker, A.; Gopalakrishnan, G. C., A decision procedure for geometry in Coq, Theorem Proving in Higher Order Logics, 225-240 (2004), Heidelberg: Springer, Heidelberg · Zbl 1099.68734
[19] Obrecht, C.: Eukleides, http://www.eukleides.org/
[20] Quaresma, P., Janičić, P.: Framework for constructive geometry (based on the area method). Technical Report 2006/001, Centre for Informatics and Systems of the University of Coimbra (2006) · Zbl 1188.68264
[21] Quaresma, P., Janičić, P.: GeoThms - geometry framework. Technical Report 2006/002, Centre for Informatics and Systems of the University of Coimbra (2006) · Zbl 1188.68264
[22] Quaresma, P.; Janičić, P.; Borwein, J. M.; Farmer, W. M., Integrating dynamic geometry software, deduction systems, and theorem repositories, Mathematical Knowledge Management, 280-294 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68264
[23] Quaresma, P.; Pereira, A., Visualização de construções geométricas, Gazeta de Matemática, 151, 38-41 (2006)
[24] Richter-Gebert, J.; Kortenkamp, U., The Interactive Geometry Software Cinderella (1999), Heidelberg: Springer, Heidelberg · Zbl 0926.51002
[25] Cabri Web site, http://www.cabri.com
[26] Cinderella Web site, http://www.cinderella.de
[27] Geometer’s Sketchpad Web site, http://www.keypress.com/sketchpad/
[28] Wang, D.: Geother (geometry theorem prover), http://www-calfor.lip6.fr/ wang/GEOTHER/ · Zbl 1412.68266
[29] Wang, D.; Winkler, F., GEOTHER 1.1: Handling and proving geometric theorems automatically, Automated Deduction in Geometry, 194-215 (2004), Heidelberg: Springer, Heidelberg · Zbl 1202.68390
[30] Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Proceedings of UITP 2005, Edinburgh, UK (April 2005)
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.