2. GEO - a collection of mechanized geometry theorem proofs

As a second application of our general framework we collected examples from mechanized geometry theorem proving scattered over several papers mainly of W.-T. Wu, D. Wang, and S.-C. Chou, but also from other sources. The corresponding GEO table contains about 250 records of examples, most of them considered in Chou's elaborated book [3].

The examples collected so far are related to the coordinate method as driving engine as described in [3]. The automated proofs may be classified as constructive (yielding rational expressions to be checked for zero equivalence) or equational (yielding a system of polynomials as premise and one or several polynomials as conclusion).

To distinguish between the different problem classes we defined a mandatory tag prooftype that must be one of several alternations defined in the Syntax attribute in the corresponding meta sd-file. Extending/modifying this entry modifies the set of valid proof types. Hence the table is open also for new or refined approaches.

According to the general theory, see, e.g., [3], for a geometry proof in the framework under consideration one has to fix

• lists of independent (tag parameters) and, for equational proof type, dependent (tag vars) variables,
• formulas for the coordinates (tag coordinates) of all intermediate points, lines etc.,
• for equational problems, the polynomial conditions defining the relations between the dependent variables (tag polynomials),
• the conclusion polynomial(s) (tag conclusion),
• and possibly polynomial inequalities (tag constraints) which are required to be satisfied since the conclusion is invalid in general.

Further, we collect some background information of relational type and, for equational problems, also a ``proof'' (tag solution).

At the moment the background information consists of a reference to PROBLEMS as foreign table which points to a statement of the geometry theorem and, for equational type, a reference to the corresponding polynomial system in the INTPS table. References to bibliography entries are handled as above, i.e., GEO is considered as foreign table and the references are attached to BIB records.

We follow the spirit of [3] and collect not only the corresponding polynomial systems but also the way they are created from the underlying geometric configuration, i.e., the corresponding code of a suitable geometry software. To study aspects of code reusability and generality we took the GEOMETRY package [5] of the second author as base, that meanwhile exists in versions for REDUCE, MAPLE, MATHEMATICA, and MUPAD.

Due to different restrictions (case sensitivity, principal syntax differences), the code which describes a geometric statement in the GEOMETRY package language (Geo code, for short) varies between different CAS, but in a way that can be handled automatically. The tag values of coordinates, polynomials etc. contain code in a generic language that can be processed by Perl tools to generate correct Geo code for the different CAS. The design of this generic language may serve as a prototype also for other tables that store CAS code. We will not embark into details here, since this part works well for the special application but is yet under development.

The solution tag value contains code that is generic in a more obvious way. In most cases it contains the lines

sol:=geo_solve(polys,vars);
geo_eval(con,sol);

or

gb:=geo_gbasis(polys,vars);
geo_normalf(con,gb,vars);

where polys, vars, and con are assumed to be CAS variables that contain the polynomial conditions, variables, and conclusion and geo_solve, geo_eval, etc., are appropriate procedures for solving, evaluation, Groebner basis and normal form computation, that are defined in special interface packages, one for each CAS, in terms of the respective functionality of the given CAS. To really prove one of the given geometry theorems, the respective CAS must load the interface package as init-file and the SYMBOLICDATA tools must translate the given tag value into syntactically correct input for the given CAS.