GeoThms --- a Web System for Euclidean Constructive Geometry



GeoThms is a web-based framework for exploring geometrical knowledge that integrates Dynamic Geometry Software (DGS), Automatic Theorem Provers (ATP), and a repository of geometrical constructions, figures and proofs. The GeoThms users can easily use/browse through existing geometrical content and build new contents. In this paper we describe GeoThms functionalities, focusing on the interface solutions required for a system aimed at supporting studying and teaching geometry via Internet. GeoThms is a publicly accessible system with a growing body of geometrical constructions and formally proven geometrical theorems. We believe that, with the help of all its users it will become an important Internet resource for geometry.


Web interfaces for proof systems; automated geometry theorem proving; dynamic geometry software


Automated theorem proving


Electronic Notes in Theoretical Computer Science, Vol. 174, #2, pp. 35-48, Elsevier, May 2007

Cited by

Year 2015 : 2 citations

 Botana, F., Hohenwarter, M., Janicic, P., Kovács, Z., Petrovic, I., Recio, T., & Weitzhofer, S. (2015). Automated theorem proving in GeoGebra: current achievements. Journal of Automated Reasoning, 55(1), 39-59.

 Chen, X., Song, D., & Wang, D. (2015). Automated generation of geometric theorems from images of diagrams. Annals of Mathematics and Artificial Intelligence, 74(3-4), 333-358.

Year 2014 : 2 citations

 Chen, Xiaoyu, Representation and automated transformation of geometric statements, JSSC 27,2. Doi: 10.1007/s11424-014-0316-0

 Chen, Xiaoyu and Song, Dan and Wang, Dongming, Automated generation of geometric theorems from images of diagrams, Annals of Mathematics and Artificial Intelligence, Springer 2014. Doi: 10.1007/s10472-014-9433-7

Year 2013 : 1 citations

 Formalization and Specification of Geometric Knowledge Objects, X Chen, D. Wang. Mathematics in Computer Science, 2013 - Springer

Year 2012 : 2 citations

 A combination of a dynamic geometry software with a proof assistant for interactive formal proofs, Pham, T.M., Bertot, Y., Electronic Notes in Theoretical Computer Science volume 285, issue , year 2012, pp. 43 - 55

 Xiaoyu Chen, Interfacing Euclidean Geometry Discourse with Diverse Geometry Software (Extended Abstract), Informatics Research Report, ADG2012, School of Informatics, University of Edinburgh, 2012.

Year 2010 : 1 citations

 Janicic, Predrag, Geometry Constructions Language, JAR 44(1-2). Doi:10.1007/s10817-009-9135-8