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 popular 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 possible 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. Unfortunately, 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 suficient to attack certain inequality exploration problems and they can be later substitutes/alternatives for the general RQE tool in our framework.
Complex algebraic geometry and real quantifier elimination (RQE) approaches can solve
nontrivial elementary geometry problems in the field of automated theorem proving, see [
Automated reasoning for equational constraints based on, for example, Gröbner basis
techniques is already available in some DGS, such as GeoGebra, see [
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 [
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 inequalities 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
[
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.
In the field of efective 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 [
Many scientific papers report about success in automated reasoning in geometrical
inequalities, see e.g. the BOTTEMA prover in [
Our recent work contributes also to the publicly available test problems in this field by providing the investigated problems in various formats.
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 [
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 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 [
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 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 [
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 [
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 [
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 [
IT
IRT
ET GIEPT
RT CF
CB-1 WLOG0
WLOGa
WLOGc RQE
PRF 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 [
In this section we report on testing the general CF variants of the seven problems above with 5 diferent 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: (1) (2) ∃ > 0 ∧ 1 + > ∧ 1 + > ∧ + > 1 ∧ > 0 ,, ∧ ( + + 1) · ( + − 1) · (1 + − ) · (1 + − ) · 2 = 2 · 2 ∧ (1 + + ) = · .
All five tools solve the problem and return an output formula equivalent to
0 < ≤ 3√3.
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.
• 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 homogeneous 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.
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 [
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 diferent 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 diferent points , are chosen to form an isosceles triangle. The diferent construction paths lead to diferent (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).
∃ 8,11,13,14 > 0 ∧ 11 > 0 ∧ 13 > 0 ∧ 14 > 0 ∧ 8 − 123 = 0 2 ∧ 82 − 124 + 1 = 0 ∧ 14 82 − 121 + 14 = 0 ∧ ∧ 1 + 13 + 14 = · 11.
(3)
4 < ≤ 2 + 2√2. (4)
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 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 [
Comparison of speed of the two diferent approaches should be addressed by future work.
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 dificult 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 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.
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 [
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 ∧ 8 − 124 + 1 = 0
2 ∧ 82 − 123 = 0 ∧ 14 82 − 121 + 41 = 0 ∧ (1 + 13 + 14) = · 11. (5) 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 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 [
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 diferent 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 suficient 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 [
We investigated the possibility of the automatic exploration of geometric inequalities based on RQE methods. We tested five available RQE tools which ofer various diferent algorithms for performing efective 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
ifnding, see also [
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) numerically obtained bounds and thus, as a pre-processing step, by narrowing the search space, they may contribute to the eficiency 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.
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 Development Fund).