Many hard examples in Polynomial Systems Solving originate from problems in Geometry Theorem Proving. Geometric configurations and constraints can be formulated as algebraic conditions on the coordinates of the geometric objects within the configuration. A main road of mechanized geometry theorem proving is such a translation of geometric into algebraic problems about Polynomial Systems Solving, and such examples of algebraic problems were collected within SymbolicData version 1. A large collection of examples from S.C. Chou’s famous book was supplied by Malte Witte in 2001 (at those times student at Leipzig Univ.).
Starting from such a more algebraic point of view, with SymbolicData version 2 H.-G. Gräbe developed a (functional) geometric language for Geometry Straight Line Programs, the GeoCode language, to describe the dynamic geometric nature of those examples directly. These descriptions introduce a more concise distinction between basic dynamic elements (movable points and sliders), geometric constructions (building up the whole picture step by step from the basic dynamic elements), geometric constraints (boolean constraint conditions that translate algebraically into zeroes of rational expressions) and geometric conclusions (boolean conditions, too).
These descriptions can be used as input to the GeoProver Software that aims to translate the problem settings from the generic language into polynomial systems syntax to be solved with the target CAS (Maple, Mathematica, MuPAD, Reduce for the moment).
During redesign it turned out that there is a close relation to the description of drawings within Dynamical Geometry Software (DGS). The main difference is in the nature of variables for geometric objects - the SymbolicData descriptions (SD version 2) used a call by value semantics for geometric objects, the variable semantics in DGS is call by reference since all even intermediate geometric objects (even hidden ones) are required to generate the drawing and to track the dynamics. The main difference between both semantics is that a call by value semantics allows for nested function calls, but a call by reference semantics requires function calls with explicit variable names as parameters.
To change the semantics required to denest nested geometric function calls, i.e., to transform the geometry problems from a weak (or extended) Geometry Straight Line syntax, allowing nested function calls, to a strong Geometry Straight Line syntax without nested function calls. This was done during the relaunch of SymbolicData version 3.
The SymbolicData collection contains