=Paper=
{{Paper
|id=Vol-2752/paper15
|storemode=property
|title=GeoGebra and the realgeom Reasoning Tool
|pdfUrl=https://ceur-ws.org/Vol-2752/paper15.pdf
|volume=Vol-2752
|authors=Róbert Vajda,Zoltán Kovács
|dblpUrl=https://dblp.org/rec/conf/cade/VajdaK20
}}
==GeoGebra and the realgeom Reasoning Tool==
https://ceur-ws.org/Vol-2752/paper15.pdf
GeoGebra and the realgeom Reasoning Tool
Róbert Vajdaa , Zoltán Kovácsb
a
Bolyai Institute, University of Szeged, H-6720 Szeged, Aradi vértanúk tere 1., Hungary
b
The Private University College of Education of the Diocese of Linz, A-4020 Linz, Salesianumweg 3, Austria
Abstract
Reasoning tools for geometric equalities based on elimination methods are already integrated in some
dynamic geometry systems (DGS), in particular in GeoGebra. However, no reasoning tools in any pop-
ular DGS environments for elementary inequalities exist yet. This paper investigates if the generic real
quantifier elimination (RQE) methods and their existing implementations are mature enough from the
practical point of view to explore simple elementary Euclidean triangle inequalities and the best pos-
sible geometric constants occurring in the inequalities. It is known, that from a theoretical point, real
geometry inequality problems can be cast as RQE problems and can be solved by RQE algorithms. Unfor-
tunately, the computational complexity of the RQE algorithms is rather high. The practical question is,
if the RQE problem formulations for the investigated geometric inequality are tractable in a reasonable
time limit. If this is so, an RQE based geometry inequality prover may be also an integral part of DGS.
As a first experimental step, we also implemented a real reasoning tool for GeoGebra called realgeom
which uses Wolfram’s Mathematica poly-algorithmic RQE tool as an external service for solving the
semi-algebraic problem associated to the geometric inequality exploration problem. Finally, we show
by an example that parametric real root counting algorithms may be sufficient to attack certain inequal-
ity exploration problems and they can be later substitutes/alternatives for the general RQE tool in our
framework.
Keywords
automated geometry proving, benchmark problem, database, dynamic geometry software, Euclidean
planar geometry, GeoGebra, geometric inequality, Mathematica, mathematical software, QEPCAD, real
quantifier elimination, Redlog, RegularChains, SyNRAC
1. Introduction
Complex algebraic geometry and real quantifier elimination (RQE) approaches can solve non-
trivial elementary geometry problems in the field of automated theorem proving, see [11, 39, 15].
Dynamic geometry systems (DGS) are computer programs that allow the users to construct
geometric figures by creating some free points and using them to define new objects such as
lines, circles or other dependent points—later one can move the free points and see how the
construction dynamically changes.
Automated reasoning for equational constraints based on, for example, Gröbner basis tech-
niques is already available in some DGS, such as GeoGebra, see [23, 21]. That is, the system
SC2 ’20: Fifth International Workshop on Satisfiability Checking and Symbolic Computation, July 05, 2020, Paris,
France (Virtual)
vajda@math.u-szeged.hu (R. Vajda); zoltan@geogebra.org (Z. Kovács)
{ http://www.math.u-szeged.hu/~vajda/ (R. Vajda); http://matek.hu/zoltan (Z. Kovács)
0000-0002-2439-6949 (R. Vajda); 0000-0003-2512-5793 (Z. Kovács)
© 2020 Copyright for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
204
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
can prove/disprove in a geometric construction that certain quantities are equal or lines are
orthogonal or parallel to each other, independently of the choice of the free points. A summary
on the capabilities of the reasoning engine Relation Tool in GeoGebra 5 is reported in [25].
On the other hand, it is known that some other elementary geometry problems cannot be
solved by equational reasoning—that is, the problem formulation and/or its solution needs
polynomial inequalities [40]. One powerful general tool to deal with real geometry is real
quantifier elimination (RQE) [12]. In the literature there are remarkable examples which treat
some geometry problems via RQE, see [39, 19] and there are some computer algebra systems
(CAS) or dedicated software packages which offer at least one method for RQE:
1. Maple’s RegularChains based package [9]
2. Maple’s SyNRAC package [24]
3. the QEPCAD B package [13, 8]
4. the Redlog package for Reduce [18]
5. Wolfram Mathematica’s combined built-in RQE engine [42]
Still, the high complexity of the algorithms for quantifier elimination from the theoretical
side (see [17]) and the state of the art of the implementations from the practical side delay
the occurrence of these as part of a powerful reasoning tool in DGS. In particular, there is no
reasoning tool for geometric inequalities yet available in GeoGebra or in any other popular
DGS. For the problems and the didactical challenges in the application of reasoning tools in
DGS we refer to [4].
The current paper focuses only on geometric inequality exploration problems, which will be
defined in Section 3 and leave aside the easier inequality-verifying problems. On a classical set
of geometric inequalities for triangles mainly taken from [5], it explores how these problems
can be cast as RQE problems, what sort of inequalities can be discovered by RQE using the
already existing RQE implementations, which instances can be solved in a reasonable time.
As an experimental and practical first step of a larger work, our vision is the automated
proving of simple inequalities and the discovery of (linear) inequalities between two geometric
invariants. This translates to RQE problems with 2-7 variables.
The translated exploration problems are conjunctions of polynomial equations and inequali-
ties where all variables are existentially quantified except for one, which is free. That is, we do
not have quantifier alternations in the translated problems. Therefore, a direct application of
some specialized RQE process (see Section 6 and [43, Chap. 6], [40, Chap. 2.5]) may still enlarge
the real-time tractable problem class (see Section 4 for our problem-timing categories) with the
proposed method and is under investigation by the authors. We note that although a translated
problem is not a (quantifier-free) SMT instance, in fact it is very close to it and a huge part of
the parameter space may be excluded from the exploration by proving unsatisfiability of the
initial formula extended with inequalities for the free variable as a pre-processing step.
We implemented a real reasoning tool for GeoGebra called realgeom which uses Wolfram’s
Mathematica RQE tool for solving the semi-algebraic problem associated to the geometric
inequality exploration problem. The test implementation is freely available for various platforms
[22, 1]1 . We illustrate our implementation with variants of seven inequality exploration problems
1
We suggest using a Raspberry Pi 4 machine with the Raspbian operating system that provides a free educa-
tional version of Wolfram’s Mathematica.
205
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
for triangles2 . All of them are well-known inequalities that were classified and proven in [5]:
• Bottema 1.1 (sides of triangles),
• Bottema 1.19 (sides of triangles),
• Bottema 4.2 (perimeter and area),
• Bottema 5.3 (perimeter and circumradius),
• Bottema 6.1 (perimeter and sum of heights),
• Bottema 8.1 (perimeter and sum of medians),
• Bottema 11.20 (sides of (right) triangles).
For example, Bottema 1.1 stands for the inequality
3 · (𝑎𝑏 + 𝑏𝑐 + 𝑐𝑎) ≤ (𝑎 + 𝑏 + 𝑐)2 < 4 · (𝑎𝑏 + 𝑏𝑐 + 𝑐𝑎)
where 𝑎, 𝑏 and 𝑐 denote the lengths of the sides of an arbitrary non-degenerate triangle in the
plane.
We do not aim for a complete method, neither for human readable proofs, nor for the
improvement of the known underlying theoretical results.
The paper is structured as follows. Section 2 overviews the related works, benchmarks and
repositories. Section 3 gives the definition of the geometric inequality exploration scenario in
the GeoGebra/DGS framework. Section 4 gives the hierarchy of inequality exploration problems
and their formulation as coordinate free (CF) RQE problems. Section 5 gives the formulation
and the test results for the coordinate based (CB) GeoGebra-generated examples. Section 6
gives a detailed example of a problem formulation as real parametric root finding problem (PRF).
Section 7 concludes the paper.
2. Related Work, and CAD, SMT Repositories
In the field of effective real quantifier elimination quite interesting and new theories and
implementations arose over the last decade. Not only were Collins’ Cylindrical Algebraic
Decomposition (CAD) based RQE algorithm and Weispfenning’s Virtual Substitution (VS) RQE
method refined and improved and their powers were combined, but a new, regular chains based
CAD approach also has emerged [9]. To our knowledge the five RQE tools investigated in
the current work (RegularChains version 2548, QEPCAD version B 1.72, Redlog version 3258,
SyNRAC 2016, Wolfram Mathematica 12.1) cover almost all the practical implementations which
are available now for a user. The various tools were separately applied to solve many scientific
problems and cited in many works (for references see [40]), but only very recently were their
performance compared in practice, too, see [6]. This paper is also among the first ones which
compares them for automated geometry inequality proving.
Many scientific papers report about success in automated reasoning in geometrical inequali-
ties, see e.g. the BOTTEMA prover in [43]. However, in certain sub-problem classes, in particular
for inequalities that contain nonlinear real arithmetic and (arbitrarily quantified) Tarski for-
mulas, there are only a few public repositories available with clearly formatted problems. It
2
In addition, a benchmark suite of more than 100 test cases is available at [14].
206
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
is worth to mention the Redlog Remis database [36] which contains RQE problems, about
15 of them being elementary geometry problems. Another repository [7] is maintained by
Wilson at the University of Bath—it contains 80 input formulas in Maple and QEPCAD format,
but these are typically not classical planar Euclidean geometry problems. It is also important
to mention the web repository GeoThms [33], where a rich list of related geometry proving
tools, DGS are also given—this database contains, however, only equational theorems. The
importance of standardized, structured publicly available benchmark problems were noted in
the SAT/SMT community and created SMT-LIB standard format and a public library for various
logics, among them for QF_NRA (quantifier free nonlinear real arithmetic) and NRA (nonlinear
real arithmetic), see [38]. We acknowledge that the support for the SMT-LIB format [20], [41]
and the integration of computer algebra systems and SMT-solvers [20] reached a mature level
now.
Our recent work contributes also to the publicly available test problems in this field by
providing the investigated problems in various formats.
3. Exploration of Inequalities in DGS
In this section the geometry inequality exploration scenario and the functionalities of an
integrated reasoning tool of a DGS is described. The section is written from a computer user’s
perspective, presumably from a mathematics teacher’s or student’s point of view.
That is, we assume that the user is familiar with the usual DGS construction steps in planar
geometry. For the sake of simplicity, we consider triangle constructions. It is important that the
user can label and refer to some invariants of the constructed triangles. That is, if the lengths of
the triangle sides (𝑎, 𝑏, 𝑐), the circumradius (𝑅), the heights (ℎ𝑎 , ℎ𝑏 , ℎ𝑐 ) or medians (𝑚𝑎 , 𝑚𝑏 , 𝑚𝑐 )
are needed, the user is expected to be able to construct the according segments by using the
standard tools of the DGS. We also allow to form a polynomial expressions of these quantities.
In this way we may refer to the perimeter of triangle as the sum of the triangle sides (𝑝 =
𝑎 + 𝑏 + 𝑐) or we may also form the positive integer powers of the circumradius (𝑅𝑘 , for a fixed
integer 𝑘). Now by using a dedicated tool, the user may specify two referenced quantities 𝒜, ℬ
occurring in the construction and ask by a command of the form Compare(𝒜, ℬ), if a nontrivial
infimum and/or supremum of the ratio 𝑚 = 𝒜 ℬ exists. Then the reasoning tool returns sharp
algebraic constants 𝑘, 𝐾 and user is informed that 𝑘 · ℬ < 𝒜 < 𝐾 · ℬ holds and possibly
(=) (=)
no sharper results for the range of the ratio exists. We note that in the case of trivial lower or
upper bound such as 𝑘 = 0 or 𝐾 = +∞, the output formula may be simpler.
As future work we may consider utilizing a knowledge base of formulas for substituting the
input of geometric invariants of a triangle by expressions of the sides or vertex coordinates of
the triangle [43, p. 240].
Our prototype implementation realgeom [35] is based on the vertex coordinates. It can be
seen as an extension of the Relation tool [25] in GeoGebra. The Relation tool can provide basic
metric information about quantities, but its capabilities are mostly constrained to decide if two
quantities are equal or not.
Now, with the new tool realgeom, interesting pieces of further information in Euclidean
planar geometry may be studied. For example, a student starts an experiment by drawing a
207
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
Figure 1: Two moments of manual exploration of the ratio 𝑝2 /𝐴 in GeoGebra
Figure 2: Automatic result on computing the ratio 𝑝2 /𝐴 in GeoGebra/realgeom
triangle 𝐴𝐵𝐶 and collecting experimental data on the quantities 𝑝 = 𝑎 + 𝑏 + 𝑐, 𝐴, and the ratio
𝑝2 /𝐴. Here we recall that 𝑝 stands for the perimeter of the triangle and 𝐴 for the area. The
experiment shows that 𝑝2 /𝐴 is minimal if the triangle is close to an equilateral triangle and the
minimal ratio is about 20.79 (see Fig. 1 for two screenshots of the experiment). By continuing
the experiment the student enters the command Compare((𝑎 + 𝑏 + 𝑐)2 ,𝑐 · ℎ𝑐 /2). Here we
recall that ℎ𝑐 stands for the height that belongs to side
√ 𝑐. Then the tool informs (see the formula
in Fig. 2) the user on the fact that (𝑎 + 𝑏 + 𝑐)2 ≥ 12 3 𝑐 · ℎ /2, for all non-degenerate triangles.
√ 𝑐
Indeed, 12 3 ≈ 20.78, so the DGS exploration is confirmed by CAS/RQE support.
The first implementation of realgeom on the top of GeoGebra uses Mathematica’s general
quantifier elimination tool [42] as an external service to get the solution (see [3] for a similar
concept). The realgeom system preprocesses the input formula that was generated by GeoGebra
coordinatization by eliminating as many variables as possible from linear equations.
We note that in our first implementation no deep explicit structural analysis of the problem
is present—the number of variables/equations/inequalities, the degree of the polynomials, or
other statistics do not influence the internal algorithm—we rely just on the poly-algorithmic
208
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
heuristic of the Mathematica tool to pick up good variable ordering or divide the problem into
sub-problems.
Later on, this analysis needs to be added to our implementation. Moreover, an internal
algorithm should be utilized to avoid closed source work. Some possible ways to go is to compile
QEPCAD or Redlog into a portable module (as it was performed for the Giac CAS for various
platforms, see [27]), or use a library like [2].
Free availability of the presented system can be crucial in an educational context. In fact,
teaching basic geometric inequalities is a part of the secondary mathematics curriculum in
many countries. Among others, the triangle inequality, or simple consequences of the law of
cosines, or discussion of constructability are typical possible uses. On the other hand, geometric
inequalities often appear at mathematics contests [29] as problems to solve. Therefore, a
computer software tool that can help in conjecturing or even in proving geometric inequalities,
seems to be a helpful step forward.
4. Hierarchy of the Inequality Exploration Problems
In this section we give an overview on a possible workflow on solving a given exploration
problem.
An important part of our research was started with looking up standard collections of
elementary geometric inequalities. As already mentioned above, the collection [5] was a very
supporting database in our work.
First of all, we observed that the simplest items in this database are the inequalities for
triangles which involve only the sides of the triangles. On the other hand, it is important to
note that the typical inequalities are given in terms of geometric invariants of the triangle,
rather than coordinates of the vertices of the triangles. Almost all inequalities enumerated
in [5, Chap 1.] are of the type above, and more than half of them are about the ratio of two
trivariate symmetric homogeneous polynomials of degree at most three, that is 𝑝1 /𝑝2 , where
𝑝1 , 𝑝2 ∈ Z[𝑎, 𝑏, 𝑐]. In later chapters of the database more invariants such as radii, altitudes,
medians of the triangle come into play.
We built up our own test database in an own fork of the GeoGebra DGS at GitHub at
https://github.com/kovzol/geogebra, in folder test/scripts/benchmark/compare/tests,
based mostly on the Bottema collection. For this paper we selected 7 benchmark problems,
namely the ones given in Section 1. That is, the examples 1.1, 1.19, 4.2, 5.3, 6.1, 8.1 and 11.20
were chosen for testing and we decided to investigate their variants. As we will see, several
variants of a geometry-inequality exploration problem (GIEP) can exist. On the one hand we
may need to test the inequality problems not only for general (non-degenerate) triangle (GT),
but also for
• isosceles triangles (IT),
• right triangles (RT),
• isosceles right triangles (IRT), and
• equilateral triangles (ET).
On the other hand, variants of the given problem can exist also in terms of the algebraic
formulation of the problem: the formulation can be coordinate free (CF) as it appears in [5] or
209
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
GIEPT
GT IT RT IRT ET
CF CB-1
WLOG0 WLOGa WLOGc
RQE PRF
Figure 3: Structure of the analysis of the exploration problem
coordinate based (CB), as in our case, and the latter is also dependent of the particular DGS
construction which were used to construct certain quantities or the triangle itself.
Finally, in fact, as usual, some variables of the semi-algebraic formula which encodes the
inequality problem may be specialized to a constant to reduce the complexity of the algebraic
problem (for instance, by putting one vertex of a triangle to (0, 0) or assuming that the side
of the triangles satisfy that 𝑎 ≤ 𝑏 ≤ 𝑐 = 1). Depending on the decision of the particular
specializations, again, several problem-variants may be derived for the same GIEP.
Fig. 3 shows an illustration of types and hierarchy of the exploration of a geometry-inequality
problem (GIEPT). On the top level, a triangle class is selected: a (non-degenerate) general
triangle (GT) or the same problem for a specialized triangle class (IT, RT, IRT, ET). Instead of
investigating the problem for general triangle (GT), the analysis of the specialized right triangle
(RT) variant will be given in detail.
On the next level, a decision must be made if the computation will be a coordinate-free
(CF) or a certain coordinate-based one (CB-1, CB-2, . . .)—note that there are several ways to
describe the same GIEP problem with coordinates. As a next decision, the algorithm must
decide if the variables remain as general as possible (WLOG0, that is, no “without loss of
generality” assumption will be made), or, eventually the cathetus 𝑎 (WLOGa) or the hypotenuse
𝑐 (WLOGc) will be substituted by a particular value—“without loss of generality”. (See [16] for
a short summary on the topic.) Finally, the underlying computation system may have multiple
choices on selecting the best fitting “real” algorithm, namely an RQE or a PRF based calculation.
Since Fig. 3 is just a partial illustration, the full structure in the background is usually more
complicated.
210
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
Table 1
Performance of various RQE tools for the general CF benchmarks
B-T-CFC7 Solved (ST+S2+S3) Solved in Time (ST)
Mathematica 7/7 6/7
QEPCAD 5/7 5/7
RegularChains 5/7 5/7
Redlog 5/7 5/7
SyNRAC 5/7 5/7
4.1. Testing 7 CF variants with 5 RQE tools
In this section we report on testing the general CF variants of the seven problems above with
5 different RQE tools (see Table 1, the abbreviation B-T-CFC7 stands for “Bottema’s triangles,
coordinate-free cases, 7 tests”). This preliminary research founded our further work to select
the most suitable system for the additional steps in our study.
To illustrate this variant let us consider the problem Bottema 5.3, where inequalities for the
ratio of 𝒜 = 𝑎 + 𝑏 + 𝑐 and ℬ = 𝑅 (perimeter and circumradius) are given. Without loss of
generality we can assume that 𝑎 = 1, to reduce the number of variables. We formulate the RQE
problem as follows:
∃ 𝑚>0 ∧ 1+𝑏>𝑐 ∧ 1+𝑐>𝑏 ∧ 𝑏+𝑐>1 ∧ 𝑅>0
𝑏,𝑐,𝑅
∧ (𝑏 + 𝑐 + 1) · (𝑏 + 𝑐 − 1) · (1 + 𝑏 − 𝑐) · (1 + 𝑐 − 𝑏) · 𝑅2 = 𝑏2 · 𝑐2 (1)
∧ (1 + 𝑏 + 𝑐) = 𝑚 · 𝑅.
All five tools solve the problem and return an output formula equivalent to
√
0 < 𝑚 ≤ 3 3. (2)
Not all the investigated RQE tools return syntactically exactly the formula (2). It could be
considered a canonical form of the description of the one-dimensional semi-algebraic solution
set. Moreover, some other output formula may contain real algebraic numbers as bounds either
directly in the output formula or implicitly encoded in the Tarskian language. Still, the extraction
of the needed sharp geometrical constants after some post-processing from the obtained one
variable quantifier free RQE output formula can be considered standard, the computation is
cheap, and is not described in more detail here.
For the further classification we set up four categories. In this way we can benchmark if the
investigated problem is tractable in a reasonable time limit.
• Solved in Time (ST): Problem solved in 10 sec3 . This could be considered in a real time
exploration via a DGS as reasonable time limit.
• Solved (S2): Problem solved in 300 sec. This is still promising, because some progress on
the practical implementation may bring the problem to the practically tractable class.
3
All computations were performed on a PC with Intel Core i7 3.2 Ghz, 9 GB RAM.
211
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
• Solved (S3): Problem solved less than 3600 sec, but more than 300 sec, it is interesting only
for research purposes, not for practical real time applications in the context of proving.
• Not Solved, TimeOut (TO): Not solved in one hour.
We see from the Table 1, and also further test results for problems with symmetric homoge-
neous polynomials and for [5, Chap. 1]) confirmed, that Mathematica’s poly-algorithmic tool
performed the best among the available—and for us known—RQE tools. So for further testing
and for proto-implementation, we decided to use Mathematica’s RQE.
5. Test Results of the realgeom Tool
In this section we report about the CB variants of the 7 inequality problems, which were
enumerated in Section 1. The tests and the results are available at [14] and classified into the
following 3 groups.
5.1. Isosceles and Right Triangles
Group 1 (abbreviated with B-IR-CBC7 which stands for Bottema’s database, the isosceles/right
triangles, that cover 7 cases) consists of 28 problems,
• 2 × 7 CB problems for isosceles triangles and
• 2 × 7 CB problems for right triangles.
Because of two different construction paths, for each triangle type from above and for each
inequality problem there are two variants. For example, for isosceles triangles, Version B (Ver. B)
refers to a DGS construction, where from a perpendicular bisector 𝑔 of a segment 𝐴𝐵, a point 𝐶
is chosen to form an isosceles triangle, while version A (Ver. A) indicates another construction
path: From a circle with center 𝐴 and radius 𝑏, two different points 𝐵, 𝐶 are chosen to form an
isosceles triangle. The different construction paths lead to different (although mathematically
equivalent) semialgebraic problems.
We also note that these problems also have proven theoretically important, because the
corresponding semi-algebraic problem, after a suitable specialization, can be considered as a
1-parameter problem, see Section 6.
The results generated by the realgeom tool are presented in Table 2.
For illustration, we give the exploration DGS window (construction with the usage of the
tools) and the derived semi-algebraic formula for the test case RightTriangle-Bottema5.3a
(referenced as R 5.3 in Table 2).
∃ 𝑚 > 0 ∧ 𝑣11 > 0 ∧ 𝑣13 > 0 ∧ 𝑣14 > 0 ∧ 𝑣82 − 𝑣13
2
=0
𝑣8 ,𝑣11 ,𝑣13 ,𝑣14
1 2 1
2
∧ 𝑣82 − 𝑣14 +1=0 ∧ 2
𝑣8 − 𝑣11 + =0∧ (3)
4 4
∧ 1 + 𝑣13 + 𝑣14 = 𝑚 · 𝑣11 .
212
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
Table 2
Performance of the RQE-based realgeom tool for isosceles and right triangles
B-IR-CBC7 Result Timing Ver. A (ms) Timing Ver. B (ms)
I 1.1 3√≤𝑚<4 60 73
10+8 2
R 1.1 7 ≤𝑚<4 61 60
1
I 1.19 3√≤ 𝑚 < 21 38 44
R 1.19 6−4 2 ≤√ 𝑚 < 12 62 60
I 4.2 𝑚 ≥ 12 3√ 66 48
R 4.2 𝑚 ≥ (12 +√8 2) 48 52
I 5.3 𝑚≤3 3 √ 1150 84
R 5.3 4 < 𝑚 ≤ (2√+ 2 2) 192 931
I 6.1 𝑚 ≤ 23 √ 216 374
1 3− 2
R 6.1 2 <𝑚≤ 2 196 9156
3
I 8.1 <𝑚<1 237 97
√ √︀ 4 √
R 8.1 5 − 3 − 5 − 21 ≤ 𝑚 < 1 4120 179494
I 11.20 𝑚 ≥ 1√ 35 35
R 11.20 1<𝑚≤ 2 42 42
Figure 4: Exploration of the ratio 𝑝/𝑅 in GeoGebra with the realgeom tool
The output formula is equivalent to
√
4 < 𝑚 ≤ 2 + 2 2. (4)
Fig. 4 shows how our implementation communicates this theorem via the Compare command,
or, in a more user-friendly way, via the Relation tool—here the user can obtain the result by
clicking the icon of the tool, then 𝑝, 𝑅, and finally on “More. . .” to compare the two lengths
symbolically.
5.2. Equilateral and Isosceles Right Triangles
Group 2 (abbreviated as B-EIR-CBC7) consists again 2 × 7 problems for equilateral, and for
isosceles right triangles. This is the easiest problem class with corresponding zero dimensional
213
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
Table 3
Performance of the RQE-based realgeom tool for equilateral and isosceles right triangles
B-EIR-CBC7 Result Timing Ver. A (ms)
E 1.1 𝑚=3 √ 60
IR 1.1 𝑚 = 10+8 7
2
61
1
E 1.19 𝑚= 3 √ 38
IR 1.19 𝑚 = 6 −√4 2 62
E 4.2 𝑚 = 12 3 √ 66
IR 4.2 𝑚 = (12√ + 8 2) 48
E 5.3 𝑚=3 3 √ 1150
R 5.3 𝑚 = (2
√
+ 2 2) 192
3
E 6.1 𝑚= 2√ 216
IR 6.1 𝑚 = 3−
√2
2
196
E 8.1 𝑚 = 23 √︀ 237
√ √
IR 8.1 𝑚 = 5 − 3 − 5 − 21 4120
E 11.20 𝑚=√ 1 35
IR 11.20 𝑚= 2 42
ideals (same amount of variables and equations in the algebraic problem) so we give here only
one variant per geometry inequality problem.
In fact, these test cases can be studied without real reasoning in a more or less satisfactory
way. After certain specialization only elimination of all variables but 𝑚 is required, and this
can be achieved via Gröbner basis computation. After obtaining an elimination ideal we learn
that it is zero dimensional and after factorization a set of possible algebraic numbers can be
obtained. Finally, excluding those that are negative we get one or more algebraic numbers.
That is, in some cases we get more than one algebraic number—for instance, the test case
IsoRightTriangle-Bottema1.19a
√ √ (abbreviated as IR 1.19 √
in Table 3) produces the possible
set {6 − 4 2, 6 + 4 2}. Actually, the correct solution 6 − 4 2 has the minimal polynomial
𝑥2 − 12𝑥 + 4 that has two positive roots, and the other root cannot be excluded without real
reasoning. Here we refer to [34, 15, 26] for further details on this approach.
Comparison of speed of the two different approaches should be addressed by future work.
5.3. General Triangles
Finally, Group 3 (B-T-CBC7) are coordinate based counterparts of the 7 problems for general
triangles (B-T-CFC7) investigated in Section 4.
We see that those coordinate based versions of the inequality problems for the general
triangles, which consist of the sides only or the sides and an extra geometric invariant, could
be handled again quite well with RQE. But two problems remained unsolved (TB 6.1, TB 8.1).
The result for the case TB 6.1 (sum of heights and perimeter) was a bit surprising, because a CF
version formulation could be solved via Mathematica’s RQE easily (cf. Table 1). The case TB 6.1
was expected (sum of medians and perimeter), because the easier CF version is proven to be
also difficult and needed more that an hour for its RQE solution. This problem is known to be
challenging geometry problem ([32, p. 86]) and we do not see at the moment a chance to solve
214
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
Table 4
Performance of RQE-based Realgeom tool for general triangles.
B-T-CBC7 Result Timing Ver. A (ms)
TB 1.1 3 ≤ 𝑚 < 4 333
TB 1.19 31 ≤ 𝑚 <√2
1
284
TB 4.2 𝑚 ≥ 12√ 3 283
TB 5.3 𝑚 ≥ 3 3 450
TB 6.1 𝑚=? TO
TB 8.1 𝑚=? TO
TB 11.20 𝑚≥1 66
it with our tool or with an improved direct RQE call in a few seconds, because it contains many
variables.
Therefore in the next section, we suggest an alternative method (PRF) for attacking problems
with many variables. We note that the all details of the alternative method is not yet elaborated
or implemented by the author.
6. Real Parametric Root Finding (PRF)
In this section we reconsider the test case Bottema 5.3 for right triangles. With this example we
demonstrate that certain geometry inequality problems can be solved without using full RQE,
that is, without building up a CAD for the space 𝑅𝑛 , where 𝑛 is defined by all the occurring
variables in the system. Instead, we need only a smaller dimensional generic CAD decomposition
(see e.g. [30, Section 2]) and some Gröbner basis computations. This method is referenced as a
variant of parametric root finding (PRF).
To utilize PRF, we assume that the input formula of the geometry exploration problem consist
of conjunctions of equations and strict inequalities and we can consider part of the occurring
variables as parameters of the system, keeping the other variables as indeterminates. If the
system is well-behaved [30] with respect to the parameters, that is, we have as many equations
as indeterminates and some auxiliary technical conditions, then generically, the system will
have only finitely many solutions with respect to a fixed parameter set. Moreover, except for a
small dimensional subset of the parameter space, which is described by the minimal discrimiant
variety (MDV), PRF is able to characterize those parameter values for which the system has
exactly 𝑘 (constantly many) solutions by cylindrically decomposing the parameter space into
open cells.
We analyse the semi-algebraic problem related to one of the coordinate based versions of
RB 5.3. with PRF. Here is the derived polynomial constraint system with equations and strict
inequalities (cf. (3)):
𝑚 > 0 ∧ 𝑣11 > 0 ∧ 𝑣13 > 0 ∧ 𝑣14 > 0 ∧ 𝑣82 − 𝑣14 2
+1=0
1 1 (5)
∧ 𝑣82 − 𝑣132
= 0 ∧ 𝑣82 − 𝑣112
+ = 0 ∧ (1 + 𝑣13 + 𝑣14 ) = 𝑚 · 𝑣11 .
4 4
The problem has 5 variables and 4 equations, that is, one less equations than variables.
Here 𝑚, 𝑣13 , 𝑣14 , 𝑣11 refer to the parameter, the sides 𝑎 and 𝑏 and the circumradius 𝑅, in an
215
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
automatically translated way in GeoGebra’s internals. Side 𝑐, the length of the hypotenuse is
not present, because due to the suitable coordinatization, it has been derived to be 1.
If we fix 𝑚, the system has only finitely many solutions, and therefore it can be also analyzed
by parametric root finding algorithms [28, 31]. It is known that for these problems RQE is an
overkill and in order to decide if the system has a real solution for a parameter value 𝑚, CAD is
needed only for 1-D space.
We expect from this a speed-up for problems with more than 5 variables. Our benchmark
problem IsoTriangle-Perimeter_CircumRadius_c from our collection—this is a variant
of I 5.3, but uses different construction steps—results in a problem with 9 variables. It times out
by RQE, but can be smoothly solved via PRF within 5 seconds.
Here, for problem (5), it is clear that the minimal discriminant variety (MDV) is given by the
polynomial
𝑝 = 𝑚(𝑚 − 4)(𝑚 + 4)(𝑚2 − 4𝑚 + 4)(𝑚2 + 4𝑚 − 4), (6)
and assuming that 𝑝 ̸= 0, the generic CAD decomposition consisting of 4 cells √ (!) reveals that
the system has finitely many (namely: four) solutions if 4 < 𝑚 < 2 + 2 2. Testing extra
the finitely many positive real roots of 𝑝, and by combining the results, we can extract again
necessary and sufficient conditions for 𝑚. Thus, we obtain the same quantifier free formula
that we have via RQE in (4).
We note that we have the same problem class for all CF and CB based formulation for isosceles
and right triangles (cf. Table 2). The treatment of the general triangle case is also possible with
the same method, but it is more involved, because we have to analyze the solution of a system
with 2 parameters.
To our knowledge, two Maple packages are available that treat general real root classification
problems without computing a full CAD for the full space [30, 10]. Their specific performance
for the triangle problems we are interested in, is yet under investigation by the authors.
7. Conclusion and Future Work
We investigated the possibility of the automatic exploration of geometric inequalities based on
RQE methods. We tested five available RQE tools which offer various different algorithms for
performing effective quantifier elimination. Our coordinate free and coordinate based problem
formulations for triangle inequality exploration problems and the first test runs indicated that
problems involving only two geometric invariants may be translated into a first order input
formula with at most seven variables (one being free among them). At least one of the tools,
namely Mathematica’s combined tool is able to solve most of the problems in a reasonable time
limit, which in our opinion is essential for exploration in a DGS in a didactical context.
We implemented a realgeom reasoning tool on top of GeoGebra, which uses Mathematica
RQE algorithm as an external service to solve the derived RQE problems. Inequalities involving
more variables or radical expressions may need an improved approach like parametric real root
finding, see also [37], [43].
Although specialized real SMT-solvers such as SMT-RAT, Z3, etc., directly cannot explore
the exact sharp constants in a geometry exploration problem, they can approve (unvalidated)
216
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
numerically obtained bounds and thus, as a pre-processing step, by narrowing the search space,
they may contribute to the efficiency of the geometric reasoning tool.
In our opinion the first steps on investigating if some RQE algorithms are already mature
enough to support learning experiments on inequalities, are done. The next steps would be to
use refined and specialized methods to explore elementary inequalities in a DGS framework.
Acknowledgments
The first author was supported by the EU-funded Hungarian grant EFOP-3.6.1-16-2016-00008.
The second author was partially supported by a grant MTM2017-88796-P from the Spanish
MINECO (Ministerio de Economia y Competitividad) and the ERDF (European Regional Devel-
opment Fund).
References
[1] Abar, C.A.A.P., Kovács, Z., Vajda, R., Recio, T.: Conectando Mathematica e GeoGebra para
explorar construções geométricas planas. Brazilian Wolfram Technology Conference, Saõ
Paulo, Brazil (2019)
[2] Basic Polynomial Algebra Subprograms (BPAS) Library, bpaslib.org. Last accessed 1 May
2020
[3] Botana, F., Kovács, Z.: A Singular web service for geometric computations. Ann. Math. Ar-
tif. Intelligence 74(3-4), 359–370 (2015)
[4] Botana F., Recio T., Velez M.P.: The role of automated reasoning of geometry statements
in mathematics instruction, CERME 10 position poster (2017)
[5] Bottema, O., Djordjevic, R.Z., Janic, R.R., Mitrinovic, D.S., Vasic, P.M.: Geometric Inequali-
ties. Wolters-Noordhoff Publishing, Groningen (1969)
[6] Bradford R., Davenport J., England M., McCallum S., Wilson D.: Truth Table Invariant
Cylindrical Algebraic Decomposition. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov,
E.V. (eds.) Computer Algebra in Scientific Computing. CASC 2014. LNCS, vol. 8660, pp.
44–58. Springer, Cham (2014)
[7] Bradford, R., Davenport, J., Wilson, D.: A repository for CAD Examples. ACM Comm. in
Comput. Alg. 46(3), 67–69 (2013)
[8] Brown, C.W.: An Overview of QEPCAD B: a Tool for Real Quantifier Elimination and
Formula Simplification. J. Japan Soc. Symb. Alg. Comput. 10(1), 13–22 (2003)
[9] Chen, C., Maza, M.M.: Quantifier Elimination by Cylindrical Algebraic Decomposition
based on Regular Chains. J. Symb. Comput. 75, 74–93 (2016)
[10] Chen, C., Maza, M.M.: Solving Parametric Polynomial Systems by RealComprehensive-
Triangularize. In: Proceedings of ICMS 2014 – 4th International Congress, Seoul, South
Korea, LNCS, vol. 8592, pp. 504–511. (2014)
[11] Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company,
Dordrecht, Netherlands (1988)
[12] Collins, G.E.: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic De-
217
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
composition. In: Caviness, B.F., Johnson, J.R. (eds.): Quantifier elimination and cylindrical
algebraic decomposition, 85–121, Springer (1998)
[13] Collins, G.E., Hong, H.: Partial Cylindrical Algebraic Decomposition for Quantifier Elimi-
nation, J. Symb. Comput. 12, 299–328 (1991)
[14] Comparison benchmark for GeoGebra 46, https://tinyurl.com/realgeom46. Last accessed
14 May 2020
[15] Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary
geometry. J. Autom. Reasoning 43(2), 203–236 (2009)
[16] Davenport, J.: What Does “Without Loss of Generality” Mean, and How Do We Detect It.
Math. in Comp. Sci. 11, 297–303 (2017)
[17] Davenport, J., Heintz J.: Real quantifier elimination is doubly exponential. J. Symbolic
Comput. 5, 29–35 (1988)
[18] Dolzmann, A., Sturm, T.: Redlog: Computer Algebra Meets Computer Logic. ACM SIGSAM
Bulletin 31(2), 2–9 (1997)
[19] Dolzmann A., Sturm, T., Weispfenning V.: A new approach for automatic theorem proving
in real geometry. J. Autom. Reasoning 21, 357–380 (1998)
[20] Forrest, S.A.: Integration of SMT-LIB Support into Maple. Second Annual 𝑆𝐶 2 Workshop,
ISSAC 2017, Kaiserslautern, Germany (2017)
[21] GeoGebra, https://www.geogebra.org/. Last accessed 1 May 2020
[22] GeoGebra Discovery, https://github.com/kovzol/geogebra-discovery/. Last accessed 14
May 2020
[23] Hohenwarter, M.: Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene.
Master’s thesis. Paris Lodron University, Salzburg (2002)
[24] Iwane, H., Yanami, H., Anai, H.: SyNRAC: a toolbox for solving real algebraic constraints.
In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 518-522. Springer, Heidelberg
(2014)
[25] Kovács, Z.: The Relation Tool in GeoGebra 5. In: Botana, F., Quaresma, P. (eds.), Post-
conference Proceedings of the 10th International Workshop on Automated Deduction in
Geometry (ADG 2014), 9-11 July 2014, LNAI, vol. 9201, pp. 53–71. Springer, Heidelberg
(2015)
[26] Kovács, Z.: Discovering Geometry Theorems in Regular Polygons. In: Fleuriot, J., Wang,
D., Calmet, J. (eds.) Artificial Intelligence and Symbolic Computation. AISC 2018. LNCS,
vol. 11110, pp. 155-169. Springer, Cham (2018)
[27] Kovács Z., Parisse B., Giac and GeoGebra – Improved Gröbner Basis computations, LNCS,
vol. 8942, 126–138 (2015)
[28] Lazard, D., Rouillier, F.: Solving parametric polynomial systems. J. Symb. Comput. 42(6),
636–667 (2007)
[29] Leng, G.: Geometric Inequalities. Mathematical Olympiad Series, Vol. 12. East China
Normal University Press, World Science Publishing (2016)
[30] Liang, S., Gerhard, J., Jeffrey, D.J., Moroz, G.: A package for solving parametric polynomial
systems. ACM Comm. Comp. Algebra 169(43), 61–72 (2009)
[31] Moroz, G.: Complexity of the resolution of parametric systems of polynomial equations
and inequations. In: ISSAC ’06: Proceedings of the 2006 international symposium on
Symbolic and algebraic computation, pp. 246–253 (2006)
218
Róbert Vajda et al. CEUR Workshop Proceedings 204–219
[32] Posamentier, A.S., Salkind, T.S.: Challenging Problems in Geometry. Dover Publications,
New York (1996)
[33] Quaresma, P., Janičić, P., GeoThms: a Web System for the Euclidean Geometry. Electronic
Notes in Theoretical Computer Science 174(2), 35–48 (2007)
[34] Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Au-
tom. Reasoning 23, 63–82 (1999)
[35] realgeom, http://github.com/kovzol/realgeom. Last accessed 15 May 2020
[36] Remis, http://www.redlog.eu/remis/. Last accessed 1 May 2020
[37] Robu, J.: Automated proof of geometry theorems involving order relation in the frame of
the Theorema project. KEPT (2007)
[38] The Satisfiability Modulo Theories Library (SMT-LIB), www.SMT-LIB.org. Last accessed 1
May 2020
[39] Sturm, T., Weispfenning, V.: Computational geometry problems in REDLOG. International
Workshop on Automated Deduction in Geometry. LNCS, vol. 1360, pp. 58–86. Springer,
Berlin, Heidelberg (1996)
[40] Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfia-
bility and their applications. Math. Comput. Sci. 11, 483–502 (2017)
[41] Vale-Enriquez, F., Brown, C.W.: Polynomial Constraints and Unsat Cores in Tarski. In:
Davenport, J., Kauers, M., Labahn, G., Urban, J. (eds.) Mathematical Software – ICMS 2018.
LNCS, vol. 10931, pp. 466-474. Springer, Cham (2018)
[42] Wolfram Research, Inc.: Mathematica, Version 12.1, Champaign, IL (2020)
[43] Yang L., Xia B.: Automated Inequality Proving and Discovering, World Scientific (2016)
219