| | | Introduction |
Aiming to build a framework for constructive geometry We have extended GCLC [DJ04][JT03], 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, is based on the area method [CGZ93][CGZ96][Nar04][QJ06]. It produces proofs that are human-readable (in LaTeX form), and with a clear justification for each proof step. It is also possible, via a conversion tool, to reason about constructions made with Eukleides [Obr][QP06]. Closely linked to the mentioned tools is GeoDB -- a database of geometry theorems. It stores geometric problems, their statements, illustrations, and proofs.
The theorem prover, the visualisation tools, and the database are "packed" in the GeoThms framework. This framework provides an Web interface where the users can easily browse through the list of geometric problems, their statements, illustrations and proofs, and also to interactively use the drawing and automatic proof tools. GeoThms is a set of PHP scripts of top of a MySQL database, and is accessible from: http://hilbert.mat.uc.pt/~geothms.
In this report we begin to present the Web interface and the MySQL database. Then we present the first ten geometric results contained in the database.
| | | Introduction |