System Description: GCLCprover + GeoThms
Authors
Abstract
Dynamic geometry tools (e.g., "Cinderella", "Geometer's Sketchpad", "Cabri", "Eukleides" visualise geometric objects, allow interactive work, and link formal, axiomatic nature of geometry (most often --- Euclidean) with its standard models (e.g., Cartesian model) and corresponding illustrations. These tools are used in teaching and studying geometry, some of them also for producing digital illustrations. The common experience is that dynamic geometry tools significantly help students to acquire knowledge about geometric objects. However, despite the fact that geometry is an axiomatic theory, most (if not all) of these tools concentrate only on concrete models of some geometric constructions and not on their abstract properties --- their properties in deductive terms. The user can vary some initial objects and parameters and test if some property holds in allchecked cases, but this still does not mean that the given property is valid.
We have extended GCLC, a widely used dynamic geometry package, with a module that allows formal, deductive reasoning about constructions made in the main, drawing module. The built-in theorem prover (GCLCprover in the following text), is based on the area method. It produces proofs that are human-readable (in LaTeX form), and with a justification for each proof step. It is also possible, via a conversion tool, to reason
about constructions made with Eukleides. Hence, the prover can be used in conjunction with other dynamic
geometry tools, which demonstrates the flexibility of the developed deduction module. Closely linked to the mentioned tools is GeoThms --- a web tool that integrates dynamic geometry tools, geometry theorem provers, and a repository of geometry theorems and proofs. This integrated framework for constructive geometry, provides an environment suitable for new ways of studying and teaching geometry at different levels.
Keywords
Dynamic Geometry Software, Automatic Theorem Proving, GeometrySubject
Automated theorem provingConference
3rd International Joint Conference on Automated Reasoning 3rd International Joint Conference on Automated Reasoning, August 2006Cited by
Year 2015 : 3 citations
Marinkovic, V. (2016). ArgoTriCS–automated triangle construction solver. Journal of Experimental & Theoretical Artificial Intelligence, 1-25.
Marinkovic, V. (2015). On-line compendium of triangle construction problems with automatically generated solutions. THE TEACHING OF MATHEMATICS, 18(1), 29-44.
Billich, M. (2015). The Area Method and Proving Plane Geometry Theorems. In Current Trends in Analysis and Its Applications (pp. 433-439). Springer International Publishing.
Year 2014 : 1 citations
Chen, Xiaoyu, Representation and automated transformation of geometric statements, JSSC 27,2. Doi: 10.1007/s11424-014-0316-0
Year 2013 : 1 citations
Chen, Xiaoyu and Wang, Dongming, Formalization and Specification of Geometric Knowledge Objects, MCS 7(4). Doi: 10.1007/s11786-013-0167-4
Year 2012 : 3 citations
Marinkovic, Vesna and Janicic, Predrag, Towards Understanding Triangle Construction Problems, LNCS 7362, Springer 2013. Doi: 10.1007/978-3-642-31374-5_9
Jiang, Jianguo, and Jingzhong Zhang. "A review and prospect of readable machine proofs for geometry theorems." Journal of Systems Science and Complexity 25.4 (2012): 802-820.
Xiaoyu Chen, Interfacing Euclidean Geometry Discourse with Diverse Geometry Software (Extended Abstract), Informatics Research Report, ADG2012, School of Informatics, University of Edinburgh, 2012.
Year 2011 : 1 citations
Génevaux, Jean-David, Julien Narboux, and Pascal Schreck. "Formalization of Wu’s simple method in Coq." Certified Programs and Proofs (2011): 71-86.
Year 2010 : 3 citations
Janicic, Predrag, Geometry Constructions Language, JAR 44(1-2). Doi: 10.1007/s10817-009-9135-8
BILLICH, M.: Verification of Geometric Statements in Dynamic Geometry Environment. Usta ad Albim BOHEMICA, ročník X, 2010, číslo 1, s. 1-7.
Billich, M., Deduction and Proving of Geometric Statements in Interactive Geometry Environment, South Bohemia Mathematical Letters, Volume 18, (2010), No. 1, 39-46.
Year 2009 : 2 citations
Challenging Mathematics In and Beyond the Classroom The 16th ICMI Study, Peter J. Taylor and Edward J. Barbeau. Chap 2 Challenges Beyond the Classroom - Sources and Organizational Issues. Petar Kenderov, Ali Rejali, Maria G. Bartolini Bussi, Valeria Pandelieva, Karin Richter, Michela Maschietto, Djordje Kadijevich and Peter Taylor
Challenging Mathematics In and Beyond the Classroom The 16th ICMI Study, Peter J. Taylor and Edward J. Barbeau. Chap 3 Technological Environments beyond the Classroom. Viktor Freiman, Djordje Kadijevich, Gerard Kuntz, Sergey Pozdnyakov and Ingvill Stedøy
Year 2006 : 1 citations
Janicic P, GCLC - A tool for constructive euclidean geometry and more than that,MATHEMATICAL SOFTWARE-ICMS 2006, PROCEEDINGS LECTURE NOTES IN COMPUTER SCIENCE 4151: 58-73 2006