System Description: GCLCprover + GeoThms



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 all
checked 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.


Dynamic Geometry Software, Automatic Theorem Proving, Geometry


Automated theorem proving


3rd International Joint Conference on Automated Reasoning 3rd International Joint Conference on Automated Reasoning, August 2006

Cited 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