Automated Reasoning Tools in GeoGebra

Zoltán Kovács, Jul 4, 2017

[i]By Tomás Recio, Zoltán Kovács and M. Pilar Vélez.[/i] GeoGebra is capable of supporting the teaching of Euclidean plane geometry theorems by using numerical and symbolic computations. For these purposes some tools for the automatic proving and discovery of geometric theorems have been developed, namely the LocusEquation and Envelope commands, the extended Relation tool and command and the Prove and ProveDetails commands. They enrich the numerical study of Euclidean geometry by using advanced computer algebra algorithms.


  • 1. Existing and new tools
  • 2. Relation tool and command demo (Euler line)
  • 3. LocusEquation (explicit)
  • 4. LocusEquation (implicit)
  • 5. Envelope
  • 6. A possible classroom scenario
  • 7. An example
  • 8. Conclusion
  • 9. Summary

1.

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:[br][list=1][*]By [b]dragging the free objects[/b] their dependent objects can be visually investigated.[br][/*][*]The [b]Relation[/b] tool helps comparing objects and obtaining relations.[/*][*]By setting the [b]trace[/b] of a constructed object on/off the movement of an object will be visualized when its parent objects are changing.[br][/*][*]The [b]Locus[/b] tool shows the trace of an object for all possible positions of a parent object (while it moves on a path).[/*][*]By typing the [b]Relation[/b] or [b]Locus[/b] [b]command[/b] in GeoGebra's Input Bar more refined information can be[br]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:[br][*]The [b]Relation tool[/b] and [b]command[/b] can be used to recompute the results [b]symbolically[/b].[/*][*]The [b]LocusEquation command[/b] refines the result of the Locus command by displaying the algebraic equation of the graphical output.[/*][*]The LocusEquation command can investigate [b]implicit loci[/b].[/*][*]The [b]Envelope[/b] 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):[br][*]The [b]Prove[/b] command to get yes/no answer on a truth a statement.[/*][*]The [b]ProveDetails[/b] command to get yes/no answer on a truth a statement with more information (including non-degeneracy or essential conditions).[/*][/list]
– Zoltán Kovács

2.

–

3.

–

4.

–

5.

–

6.

–

7.

–

8.

–

9.

–

Information