The geoDB database

The geoDB database

The geoDB database gives support to the other tools, keeping the information, and allowing for its fast retrieving whenever necessary. The database is organised in the following form (see the entity-relationship diagram for details - Figure ):

theorems

-- statements of theorems, in natural-language form, formatted in LaTeX;

figures

-- descriptions of geometrical constructions, in DGT's code (GCLC, Eukleides, or other drawing tools), they can be used for producing the corresponding figures;

proofs

-- geometrical constructions with conjectures in ATP's code (GCLCprover, or other provers), they are used for producing the corresponding proofs;

A geometric theorem can have different figures and/or proofs, made by different tools, made by different users. This fact is expressed by the 1 to n relationships between the entities "theorems" and the other two entities (see Figure ).

The database also has the following auxiliary entities:

bibrefs

-- bibliographic references, in BIBTeX format;

drawers & provers

-- information about the programs whose code is kept in the database, and with which the user can interact;

authors

-- information about the authors of the programs;

users

-- information about registered users.

computer

-- information about the computer used as the test bench.

The codeTmp and codeTmpProver tables are used to store temporary information, deleted after each session ends, for the interactive section of GeoThms.

The geoDB database is implemented in MySQL, with InnoDB transition safe type of tables, and with foreign key constraints.

The geoDB database