Towards Detection of Partial Truth via Real Geometry

Abstract

Computational algebraic geometry has already shown its great potential as the underlying tool for implementing automated reasoning algorithms in elementary geometry, in a complex numbers framework, currently available, and quite performant, at GeoGebra and GeoGebra Discovery. Although this complex-field approach is often fully operative for addressing geometry statements, not involving inequalities, over the real numbers, in our presentation we will describe our recent work concerning the specific treatement of geometry theorems over the reals, including those involving inequalities. On the one hand, we think that real quantifier elimination (RQE) is a robust tool for proving geometric statements, especially for proofs of inequalities. Thus, by combining RQE with a dynamic geometry system, a convenient user interface can be used to study non-trivial geometric inequalities in the plane. We present an updated implementation of the ProveDetails command in GeoGebra Discovery which exploits the free availability and competitive speed of the Tarski software system (based on QEPCAD B and Minisat). On the other hand, we will compare this approach with an alternate one, that tries to mimic, over the reals, the complex-geometry approach, focusing on the relevance of the truth over the real irreducible components of the hypotheses variety. This allows us to consider not just the proof of truth or falsity, but to address if a more delicate classification of truth can be obtained, similarly to the notion of “truth on parts” or “truth on components” in complex algebraic geometry.

Keywords

• eol>Automated Reasoning in Geometry
• Real Quantifier Elimination
• GeoGebra
• Partial Truth

1. Introduction

The first complete study on proving geometric statements by using real quantifier elimination (RQE) is perhaps [1], being published more than 25 years ago. Even if several improvements were contributed since then, there are still hardly publicly available software tools with a simple user interface to study and prove geometry theorems via RQE. To fill the gap, we present some recent improvements of the tool GeoGebra Discovery which makes it possible to prove non-trivial geometric statements that way.

Utilizing RQE can be unavoidable in some cases. Well-known techniques like Gröbner bases, may give an incomplete translation of the geometric setup into an algebraic system because they cannot handle inequalities.

In this research first we point to some former work [ 2, 3]. In addition, in this contribution we propose a protocol via RQE. Assume we are given a plane geometric construction in GeoGebra Discovery. The user types the input ProveDetails() where is a statement to be proven. Now, the software mechanically sets up a hypothesis formula and a thesis (as sets of logical connectives of semi-algebraic formulas) that contain the free variables 1, 2, . . . , and dependent variables 1, 2, . . . , . At this point the quantified formula ∀1∀2 . . . ∀( ⇒ ) is considered. It can be negated into the form ∃1∃2 . . . ∃( ∧ ¬ ). Now a query will be formulated for the Tarski subsystem. It optimizes the input formula by using linear substitutions and other reductions, and applies cylindrical algebraic decomposition to find a quantifier-free formula in the variables 1, 2, . . . , .

If is false, then is always true. If is true, then is false. But, in several cases, forms connectives of semi-algebraic expressions in the variables 1, 2, . . . , and the situation needs to be analyzed further. In some simple cases, is a conjunction of not-equal relations: this means that the statement is true on a disjunction of equalities which has a smaller dimension than , so we conclude that is false in the overwhelming majority of cases (that is, “false”). In another simple case, ¬ is a disjunction of some relations that contain at least one inequality: this means that the statement is true on an -dimensional subset of R (if there are no other restrictions), so we conclude that is true in a significant proportion of cases (that is, “true”).

A more detailed study of such questions is related to partial truth in complex algebraic geometry (see [4]), and is planned for future work.

2. Examples

In the following examples we discuss how our new protocol identifies the geometric problem, how it is translated to an algebraic setup, how dimension is read of, and how the RQE computations are performed. Also, a comparison with a former technique, based on Gröbner bases, is presented.

2.1. A segment is usually longer than zero

Consider the user query ProveDetails( > 0) in GeoGebra Discovery, as shown in Fig. 1.

We consider a segment with two endpoints, (1, 2), (3, 4), in the plane. The length of will be denoted by 5, that is, ℎ1 : 52 = (1 − 3)2 + (2 − 4)2 and ℎ2 : 5 ≥ 0 hold. These are our hypotheses: = ℎ1 ∧ ℎ2. Our thesis is : 5 > 0.

Without loss of generality, we can, however, assume that = (0, 0) and = ( 0, 1 ). The reason for this is that the left hand side of the thesis is a homogeneous polynomial of degree 1, therefore, if the statement holds for all 1, 2, 3, 4, except eventually for (1, 2) = (3, 4), then a similarity transformation of (1, 2, 3, 4) ↦→ (1′, 2′, 3′, 4′) = ( 0, 0, 0, 1 ) keeps all ratios of all the appearing lengths in the construction. (See also [5].) That is, a 5 ↦→ 5′ mapping keeps the same ratio, and since it is still a positive number, the case 5′ > 0 is equivalent to 5 > 0.

This approach, of course, skips the analysis of the case (1, 2) = (3, 4), but this can be ignored as “skipped on purpose”. In fact, it is implicitly assumed that points and are diferent, if the user creates them as two arbitrary points. That is, our new protocol just acknowledges the intuitive purpose of the user.

Now, after substituting the assumption = (0, 0) and = ( 0, 1 ) into the hypothesis, we get the statement : ∀5(52 = 1 ∧ 5 ≥ 0 ⇒ 5 > 0) whose negation has the form ∃5(52 = 1 ∧ 5 ≥ 0 ∧ 5 ≤ 0) ( 1 ) which is clearly false. That is, is always true. We have to be, however, careful, because we implicitly assumed that ̸= . That is, the correct communication of the protocol is the following statement: “If ̸= , then > 0.”

Technically, after the user constructs , and , and issues the command ProveDetails( > 0), GeoGebra Discovery sets up ( 1 ) and asks Tarski to perform RQE by issuing a command like (qepcad-api-call [ex v5 [(v5^2-1=0) /\ (v5>=0) /\ (~(v5>0))]). This returns false, so GeoGebra Discovery outputs the result {true, {"AreEqual(A,B)"}}. This is to be interpreted: “If and difer, then the statement is true.”

2.2. A segment is usually longer than another one

We continue our first example: Consider the user query ProveDetails( > ) as shown if Fig. 2. We forget the substitutions for the coordinates 1, 2, 3, 4 at the first sight. Let us add a new point (6, 7) and another segment = . Also, we introduce 8 to express the length : ℎ3 : 82 = (3 − 6)2 + (4 − 7)2, ℎ4 : 8 ≥ 0. To express that , and form a non-degenerate triangle, we assume that

⎛1 2 1⎞ ℎ5 : 9 · det ⎝3 4 1⎠ − 1 = 0 6 7 1 by using Rabinowitsch’s trick1 for a negation. (This could be avoided in real geometry, but at this point of our research, we chose to use this method which was borrowed from the old protocol.)

These are our hypotheses: = ℎ1 ∧ ℎ2 ∧ ℎ3 ∧ ℎ4. Our thesis is : 5 > 8, or equivalently, 5 − 8 > 0.

Again, we are allowed to set up some substitutions. = (0, 0) and = ( 0, 1 ) are considered again, for the same reason as above. (Here we confirm that the expression 5 − 8 from is a degree 1 homogeneous polynomial.) On the other hand, cannot be specialized. At the end of the day, our statement has the form ∀5, 8, 9(52 = 1 ∧ 5 ≥ 0 ∧ 82 = 62 + (1 − 7)2 ∧ 8 ≥ 0 ∧ − 69 − 1 = 0 ⇒ 5 > 8) – here we note that for the free point we removed both of its variables 6, 7 from the list of quantified variables because we want to learn a condition for the truth. Now, the last formula has the negated form ( 2 ) ( 3 ) ∃5, 8, 9 (52 = 1 ∧ 5 ≥ 0 ∧ 82 = 62 + (1 − 7)2 ∧ 8 ≥ 0 ∧ − 69 − 1 = 0 ∧ 5 ≤ 8) which is equivalent to 6 ̸= 0 ∧ 6 − 27 + 72 ≥ 0

2 after performing RQE.

Geometrically, this problem is a two-dimensional one, in the variables 6, 7 of point . Therefore, to learn the truth about statement we should analyze ( 3 ): how much part of R2 is covered by the non-solutions? Is it possible that ( 3 ) is a zero-dimensional set? If yes, we can say, that is false on a “small” subset of R2. But, we should keep in mind, that such analysis should 1Let ∈ Q[1, 2, . . . , ]. To express ̸= 0, we can use the equivalent formula +1 · − 1 = 0. See [6]. be performed automatically and quickly enough. So, without answering this question at the moment, we also consider the positive variant of and compute the negation of ( 3 ), by hoping that the other formulation will be simpler to study. We get Now we hope for the best about the RQE implementation and assume that all parts of the ( 4 ) is in its simplest form, that is, for example, the quadratic inequality part is a two-dimensional set2. (See Fig. 3 for a visualization of ( 4 ): (6, 7) ↦→ (, ).) Here, by using a very simple algorithm, we can conclude that there is a two-dimensional subset of R2 on which holds, because ( 4 ) is a disjunction of sets, and one of them is an inequality of type <, ≤ , ≥ or >.

Note that it is inconvenient to see 6 = 0 in ( 4 ) because we excluded it in hypothesis ℎ5. But we note that ℎ5 is a one-dimensional restriction for the possible set of points in statement , so we are still on the safe side when ignoring that one-dimensional “noise” in the output.

Actually, the obtained circle meets our expectations because it exactly describes those points such that > is implied.

Technically, after the user constructs and , and issues the command ProveDetails( > ), GeoGebra Discovery sets up ( 2 ) and asks Tarski to perform RQE by issuing a command like (qepcad-api-call [ex v5,v8,v9 [v5^2=1 /\ v5>=0 /\ v8^2=v6^2+(1-v7)^2 /\ v8>=0 /\ -v6 v9-1=0 /\ v5<=v8]]). This returns 6 ̸= 0∧72− 27+62 ≥ 0 which requires further investigation, so Tarski’s (t-neg %) command is used to get 6 = 0∨72 − 27 +62 < 0. Finally, GeoGebra Discovery outputs the result {true, {"..."}, {"c"}} which means that the statement is true on a remarkable subset of all possible values of , but it is too dificult for the program to give a more precise explanation. (Here c recalls the abbreviation of “component” from the old protocol.)

2.3. The Triangle Inequality and a generalization of the Pythagorean Theorem

Let us continue our example by adding segment ℎ = (see Fig. 4). This requires the addition of two further hypotheses: ℎ6 : 120 = (1 − 6)2 + (2 − 7)2, ℎ7 : 10 ≥ 0. W.l.o.g. we assume again that = (0, 0) and = ( 0, 1 ). This turns ℎ6 into 120 = 62 + 2. 7

When performing our protocol given above, the following Tarski command studies if the Triangle Inequality + > ℎ holds: (qepcad-api-call [ex v5,v8,v9,v10 [v5^2=1 /\ v5>=0 /\ v8^2=v6^2+(1-v7)^2 /\ v8>=0 /\ -v6 v9-1=0 /\ v10^2 = v6^2+v7^2 /\ v10 >=0 /\ ~(v5+v8>v10)]]), and it returns false, this means that the statement always holds (under the non-degeneracy conditions ̸= and that △ is non-degenerate, this is communicated by GeoGebra Discovery with the output {true, {"AreCollinear(A,B,C)", "AreEqual(A,B)"}}).

Similarly, we can study some diferent statements. Alternatively, when checking if + < ℎ holds, we get 6 ̸= 0 for the negated condition and therefore 6 = 0 for the positive condition. That is, this statement can be true at most on a zero-dimensional subset of R2, thus it is considered false.

Let us study some variants of the Pythagorean Theorem. As well-known, in a right triangle 2 + 2 = ℎ2 holds. But here we do not assume a right triangle, so we are interested, in general, in what prerequisities are required for 2 + 2 = ℎ2. By following our protocol, we only have to change the negated thesis to ~(v5^2+v8^2=v10^2) and we obtain 6 ̸= 0 ∧ 7 − 1 ̸= 0 which can be studied better in its positive form: 6 = 0 ∨ 7 − 1 = 0. This clearly means that △ must be degenerate (which is disallowed) or the second coordinate of must be 1 (which is 2For example, a form like 62 +72 ≤ 0 would be deceptive. It is an inequality and seems to describe a two-dimensional subset of R2, but in fact it is equivalent to (6, 7) = (0, 0) which defines a zero-dimensional set. That is, we assume that the RQE implementation communicates such a subset in the “simplest” form 6 = 0 ∧ 7 = 0 and not like 62 + 72 ≤ 0. exactly the expected prerequisite that at vertex the angle is right). Since both parts of the disjunction are one-dimensional, they cannot be considered as a “large enough” subset of R2. Therefore, the Pythagorean Theorem without its well-known assumption has to be considered false.

Here we remark, that the above mentioned negative form 6 ̸= 0 ∧ 7 − 1 ̸= 0 is a conjunction of ̸= relations. In all such cases the statement is clearly false. From an algorithmic perspective means that the computation of the positive form can be skipped.

One might also be interested in whether 2 + 2 > ℎ2 holds in general. By modifying the input accordingly, we obtain the negative form 6 ̸= 0 ∧ 7 − 1 ≥ 0 which has the positive form 6 = 0 ∨ 7 − 1 < 0. This is clearly a two-dimensional subset of R2 because of the inequality part. By contrast, 2 + 2 ≤ ℎ2 also holds in general, because its positive form, 6 = 0 ∨ 7 − 1 >= 0 is also a two-dimensional subset of R2. This leads to the interesting fact that, in some sense, a thesis and also its negation ¬ can be true at the same time.

3. Comparison of the old and the new protocol

We give an example to compare the old and new protocols. The old approach computes an elimination ideal to learn the required prerequisities for a statement to be true.

Let us consider a simplified, degenerate version of the Triangle Inequality. Let us assume that = (0, 0), = ( 0, 1 ), and = (0, 7), moreover let ℎ1 : 82 = (1 − 7)2 and ℎ2 : 120 = 72. We would like to prove that : 8 + 10 = 1.

The old protocol [4] is based on elimination over the field of coeficients (usually Q) and gets geometric conclusions over the complex numbers. Since it deals with polynomials and not equations, we consider the hypotheses and the thesis as polynomials, that is, ℎ1 = 82 − (1− 7)2, ℎ2 = 120 − 72, = 8 + 10 − 1. The old protocol performs the following steps: 1. We identify a maximum-size set of independent variables. Here it is {7}. 2. The elimination ideal 1 = ⟨ℎ1, ℎ2, 11 · − 1⟩ ∩ Q[7] is computed (here 11 is a new dummy variable, to support Rabinowitsch’s trick). If 1 difers from the zero ideal, then the statement is generally true, possibly under certain conditions (that are contained in 1). In our case, 1 = ⟨0⟩, so we continue. 3. Otherwise, the elimination ideal 2 = ⟨ℎ1, ℎ2, ⟩ ∩ Q[7] is computed. If 2 difers from the zero ideal, then the statement is generally false. In our case, 2 = ⟨0⟩, so we continue. 4. Otherwise, the statement is true on components. To identify the components, for example, Maple’s command PrimaryDecomposition can be helpful, by using the hypotheses as input. Here, the primary decomposition of ℎ1, ℎ2 gives the output ⟨10 ± 7, 7 ± 8 − 1⟩, that is, it consists of 4 components, and it can be interpreted that on some components |8 − 10| = 1 holds.

In fact, from the geometrical point of view, these components belong over the reals to the cases 7 < 0, 0 ≤ 7 ≤ 1 and 1 < 7. Algebraically, however, there is a 4th, “invisible” case. This can be checked when is changed to the thesis ′ : (8 + 10 − 1) · (8 + 10 + 1) · (8 − 10 − 1) · (8 − 10 + 1) = 0, and here the second factor does not have a geometrical meaning (but all other three factors do, see also [7]).

By contrast, the new protocol performs the following steps: 1. We determine the “naive dimension” of the independent variables. Here the only independent variable is {7}, so = 1. 2. We collect all dependent variables. Here they are 8 and 10. 3. Perform RQE on ∧ ¬ where the dependent variables are existentially quantified. 4. If the result is “false”, then the statement is always true under the hypotheses. If it is “true”, then the statement is false under the hypotheses. In our case, the RQE is computed with the Tarski command (qepcad-api-call [ex v8,v10 [v8^2=(1-v7)^2 /\ v10^2=v7^2 /\ v8>=0 /\ v10>=0 /\ ~(v8+v10-1=0)]]) which yields 7 ̸= 0 ∧ 7 − 1 ̸= 0 ∧ (7 < 0 ∨ 7 − 1 > 0). ( 5 )

So we continue. 5. We determine the dimension of the result of the RQE. If < , then the statement is true under the negation (that is, the positive form) of the result of the RQE. In our case, = 1 (see below), so we continue. If cannot be determined for some reason, continue. 6. Otherwise, that is, if = , we compute the dimension of the positive form of the result of the RQE. If = , then the statement is true under the positive form of the result of the RQE. In our case, this holds. 7. Otherwise, that is, if < , the statement is false. 8. Otherwise, that is, if cannot be determined for some reason, the statement is undecided.

In our case, it is not completely straightforward how to determine . For some reason, Tarski’s output in ( 5 ) is not the simplest possible formulation, but it is equivalent to 7 ̸∈ [0, 1], and this can be confirmed by using some further basic operations in Tarski. That is, = 1, because ( 5 ) is a union of two intervals.

Finally, = 1 can be identified by negating ( 5 ) which is clearly 0 ≤ 7 ≤ 1, so we learn that the statement is true under the condition 7 ∈ [0, 1]. Geometrically, this means that the statement is true if point is an element of the segment .

In fact, the dimension of a the result of the RQE could already be obtained with some minor programming work in the Tarski subsystem. It is an on-going work to read of the dimension in such a way, and conclude truth or falsity simply and reliably.

4. Conclusion

We introduced a new protocol on proving geometric inequalities by using RQE in the educational software package GeoGebra Discovery. Our method uses the Tarski computer algebra system.

The provided examples are not completely trivial, however, using more free or dependent variables may quickly change the computational complexity infeasible. Therefore, we continue our research to automatically reduce the number of variables for a large set of possible inputs. Also, exact detection of the dimension of the RQE output is subject of future research.

Some further examples, including Viviani’s theorem and Clough’s conjecture [8] (they are, in some sense, further generalizations of the Triangle Inequality), can be found on the release announcement of GeoGebra Discovery version 2023Apr07, see https://github.com/ kovzol/geogebra/releases/tag/v5.0.641.0-2023Apr07. (See also Fig. 5 that shows a successful proof of Viviani’s theorem after computing (epc [ex sqrt3, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v5, v6, v7, v8, v9 [(v23>=0) /\ (v24>=0) /\ (v25>=0) /\ (v26>=0) /\ (sqrt3>=0) /\ (v5=-1/2) /\ (v7=1/2) /\ (v22=0) /\ (v23=1) /\ (v6=v8) /\ (v16=v10+1) /\ (v15=v9) /\ (v21=v9) /\ (v11=-v8+v9) /\ (v13=v8+v9) /\ (((v10>0) /\ ((-v9 v8+v10/2-v10+v8)>0) /\ ((v9 v8-v10/2)>0)) \/ ((0>v10) /\ (0>(-v9 v8+v10/2-v10+v8)) /\ (0>(v9 v8-v10/2)))) /\ (v8>0) /\ (sqrt3^2=3) /\ (~((-sqrt3+2 v24+2 v25+2 v26)/2=0)) /\ (4 v8^2-3=0) /\ (2 v10-2 v12-1=0) /\ (2 v10-2 v14-1=0) /\ (-v10 v17-v10 v8+v10 v9+v17 v12+v8 v18-v9 v12=0) /\ (-2 v17 v8+2 v8-v18=0) /\ (-v10 v19+v10 v8+v10 v9+v19 v14-v8 v20-v9 v14=0) /\ (2 v19 v8-v20=0) /\ (-v10^2+2 v10 v18-v18^2-v17^2+2 v17 v9-v9^2+v24^2=0) /\ (-v10^2+2 v10 v20-v20^2-v19^2+2 v19 v9-v9^2+v25^2=0) /\ (-v10^2+v26^2=0)]]) via Tarski, here the epc script is an eficient “black-box” method to compute RQE for non-trivial inputs. The epc script is maintained at https://github.com/chriswestbrown/epcx.) They contain some references to border cases when the old protocol is triggered by the program. We highlight here that in some cases the old protocol is still preferred because of substantially better speed. On the other hand, some problem settings require using real geometry, therefore the new protocol ifts much better.

Our research is made even more topical by the fact that the SC2 project has a particular focus on automated reasoning in the classroom (see [9]). Indeed, all our examples can be of educational interest, since GeoGebra Discovery ofers a familiar look and intuitive use for young learners in many languages for free of charge.

Acknowledgments

The second, fourth and sixth authors were partially supported by a grant PID2020-113192GB-I00 (Mathematical Visualization: Foundations, Algorithms and Applications) from the Spanish MICINN.

References

[1] T. Sturm , V. Weispfenning , Computational geometry problems in REDLOG , in: International Workshop on Automated Deduction in Geometry. LNCS , vol. 1360 , Springer, Berlin, Heidelberg, 1996 .

[2] S. Luksch , Ist die Computeralgebra bereit für die Unterstützung des Unterrichts der geometrischen Ungleichungen? , 2022 . URL: https://www.researchgate.net/publication/ 358210701_Bachelorthesis_Mathematik_Luksch_Simone_ WS21 .

[3] C. W. Brown , Z. Kovács , T. Recio , R. Vajda , M. P. Vélez , Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? , Mathematics in Computer Science 16 ( 2022 ) 31 . doi: 10 .1007/s11786-022-00532-9.

[4] Z. Kovács , T. Recio , M. P. Vélez , Detecting truth, just on parts, Revista Matemática Complutense 32 ( 2019 ) 451 - 474 . doi: 10 .1007/s13163-018-0286-1.

[5] J. H. Davenport , What does “without loss of generality” mean, and how do we detect it , Mathematics in Computer Science 11 ( 2017 ) 297 - 303 .

[6] J. Rabinowitsch , Zum Hilbertschen Nullstellensatz, Mathematische Annalen 102 ( 1929 ) 520 .

[7] Z. Kovács , T. Recio , C. Sólyom-Gecse , Rewriting input expressions in complex algebraic geometry provers , Annals of Mathematics and Artificial Intelligence 85 ( 2019 ) 73 - 87 . doi: 10 .1007/s10472-018-9590-1.

[8] M. de Villiers , An illustration of the explanatory and discovery functions of proof , Pythagoras 33 ( 2012 ). doi: 10 .4102/pythagoras.v33i3. 193 .

[9] I. Drămnesc , E. Ábrahám, T. Jebelean , G. Kusper, S. Stratulat, Automated reasoning in the class, Computeralgebra Rundbrief 71 ( 2022 ) 21 - 26 .