Existing and new tools
Automated reasoning tools are a collection of GeoGebra tools and commands ready to conjecture, discover, adjust and prove geometric statements in a dynamic geometric construction. First the user needs to draw a geometric figure by using certain tools. After constructing the figure, GeoGebra has many ways to promote investigating geometrical properties of a figure by various tools and settings:
- By dragging the free objects their dependent objects can be visually investigated.
- The Relation tool helps comparing objects and obtaining relations.
- By setting the trace of a constructed object on/off the movement of an object will be visualized when its parent objects are changing.
- The Locus tool shows the trace of an object for all possible positions of a parent object (while it moves on a path).
- By typing the Relation or Locus command in GeoGebra's Input Bar more refined information can be obtained. These methods are usually well known by the GeoGebra community, and therefore they are well documented. On the other hand, currently GeoGebra also offers symbolic automated reasoning tools for generalizing the observed/conjectured geometric properties:
- The Relation tool and command can be used to recompute the results symbolically.
- The LocusEquation command refines the result of the Locus command by displaying the algebraic equation of the graphical output.
- The LocusEquation command can investigate implicit loci.
- The Envelope command computes the equation of a curve which is tangent to a family of objects while a certain parent of the object moves on a path. Also some low level methods exists (only for experts or for debugging purposes):
- The Prove command to get yes/no answer on a truth a statement.
- The ProveDetails command to get yes/no answer on a truth a statement with more information (including non-degeneracy or essential conditions).