Fifth Central- and Eastern European Conference
on Computer Algebra- and Dynamic Geometry Systems
in Mathematics Education

The talk will be dual, in the sense of addressing the same issue from two different perspectives. One, that of a secondary mathematics teacher, with experience on the introduction of ATP tools (GCLC and GeoGebra) at the classroom.  Then, the point of view of a university ATP researcher and developer, with sustained involvement in math education.  In both cases the main point will be to provide some answers to the key question:

What is ATP good for?

The most efficient ATP systems in geometry are usually algebraic. Although these provers do not generate classical readable proofs, they give an yes/no answer and can generate non-degeneracy conditions (NDGs) that need to hold for the statement to be satisfied. Although ATPs can be applied to check the main statement of the theorem, we advocate that it is much more beneficial for pupils to apply automation on intermediate steps, and so to verify if their conclusions are correct and if they are on the right track to prove the main theorem. In such setting, pupils still need to produce global proof steps, while the ATP system takes care of details that are usually straightforward, but tedious to justify. Pupil cooperates with the machine and relies on its help, but his understanding of the geometry problem is still crucial for success. Trough this activity student develops his thinking and analytical skills, but, unlike with classical pen-and-paper proofs, in a very rigorous setting, since every conclusion must be precisely formulated and pass the automated test. Also, a careful analysis of NDGs may reveal many subtle issues about the theorem that is being proved. In this talk we will present some of our experience and ideas about using these techniques (implemented both in GCLC and GeoGebra) in high-school geometry classes.

Using Methods based on Automated Deduction in Geometry (ADG), it is possible to perform algebraic calculations on interactively constructed figures. Thus, a parameter of such a figure can be calculated algebraically as a function of other parameters of this figure. This opens up a new computer-assisted connection of synthetic elementary geometry to algebra. On the other hand, the question: "WHAT HOW depends on WHOM?" is cleared up when a figure is dynamically varied. - In this lecture there are given some selected examples in a constraint-based DGS developed for educational purposes. Their didactic relevance is explained and some resulting mathematics education problems are discussed.

GeoGebra is open source mathematics education software being used in thousands of schools worldwide. Since version 4.2 (December 2012) it supports symbolic computation of locus equations as a result of joint effort of mathematicians and programmers helping the GeoGebra developer team. The joint work, based on former researches, started in 2010 and continued until present days, now enables fast locus and envelope computations even in a web browser in full HTML5 mode. In conclusion, classroom demonstrations and deeper investigations of dynamic analytical geometry is ready to use on tablets or smartphones as well.

In our talk we consider some typical grammar school topics when investigating loci is a natural way of defining mathematical objects. Such topics include definition of a parabola and other conics in different situations like synthetic definitions or points and curves associated with a triangle. In most grammar schools, however, no other than quadratic curves are discussed, but generalization of some exercises and also every day problems will introduce higher order algebraic curves. Thus our talk will mention the cubic curve ``strophoid'' as locus of heights of a triangle when one of the vertices moves on a circle. Also quartic ``cardioid'' and sextic ``nephroid'' can be of every day interest when investigating mathematics in a coffee cup.

We will also focus on GeoGebra specific tips and tricks when constructing a geometric figure to be available for getting the locus equation. Among others, simplification and synthetization (via the intercept theorem) will be mentioned.

Traditionally, loci in Dynamic Geometry Systems (DGS) have been displayed either tracing the locus point, either through a special command that, roughly, enhances such tracing procedure. Some DGS incorporate more sophisticated approaches being able to return algebraic knowledge about loci. Nevertheless, these enhancements deal with a restricted type of loci, those where the position of the locus points is completely determined by another point, the mover, which must lie on a linear path. If the mover point is not unique, or it is not bound to a line, standard DGS can only offer a tracing strategy, just returning a graphical answer. Consider, for instance, two circles and a point on each circle. The locus of their midpoint is a 2-dimensional region, that cannot be easily described with current DGS.

In this talk I illustrate these limitations when computing loci. Furthermore, a discussion on the application of Cylindrical Algebraic Decomposition software will be given.