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.

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