Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories



The axiomatic presentation of geometry fills the gap between formal logic and our spatial intuition. The study of geometry is, and will always be, very important for a mathematical practitioner. GCLCprover, an automatic theorem prover (ATP) integrated with dynamic geometry software (DGS) gives its user a tool to bridge his/her spatial intuition with formal, Euclidean geometry proofs. GeoThms, a system consisting of the mentioned programs and a database geoDB, provides a framework for exploring geometrical knowledge. A GeoThms user can browse through a list of available geometric problems, their statements, illustrations, and proofs. He/she can also interactively produce new geometrical constructions, theorems, and proofs and add new results to the existing ones. GeoThms framework provides an environment suitable for new ways of studying and teaching geometry at different levels. GeoThms also provides a system for storing mathematical knowledge (in a explicit, declarative form) --- not only theorem statements, but also their (automatically generated) proofs and corresponding illustrations.


Automated theorem proving, Dynamic Geometry Software, Area Method, Geomtric Theorem Repositories


Automated theorem proving


5th International Conference on Mathematical Knowledge Management (MKM06), August 2006

Cited by

Year 2012 : 1 citations

 Janicic, Predrag, Julien Narboux, and Pedro Quaresma. "The Area Method." Journal of Automated Reasoning (2012): 1-44.

Year 2010 : 1 citations

 BILLICH, M.: Verification of Geometric Statements in Dynamic Geometry Environment. Usta ad Albim BOHEMICA, ročník X, 2010, číslo 1, s. 1-7.

Year 2007 : 2 citations

 GCLC 7.0/WinGCLC 2007 (Geometry Constructions→ LaTEX Converter) Manual

 Predrag Janicic and Pedro Quaresma, "Automatic Verification of Regular Constructions in Dynamic Geometry Systems", ADG 2006 (selected papers), LNAI 4869, pp. 39-51, 2007, Springer-Verlag Berlin Heidelberg 2007.

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