Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch’s trick

Abstract

In the algebraic-geometry-based theory of automated proving and discovery, it is often required that the user includes, as complementary hypotheses, some intuitively obvious non-degeneracy conditions. Traditionally there are two main procedures to introduce such conditions into the hypotheses set. The aim of this paper is to present these two approaches, namely Rabinowitsch’s trick and the ideal saturation computation, and to discuss in detail the close relationships and subtle differences that exist between them, highlighting the advantages and drawbacks of each one. We also present a carefully developed example which illustrates the previous discussion. Moreover, the paper will analyze the impact of each of these two methods in the formulation of statements with negative theses, yielding rather unexpected results if Rabinowitsch’s trick is applied. All the calculations have been carried out using the software Singular in the FinisTerrae 2 supercomputer.

1 Introduction

The framework of this paper is the automated theorem proving and discovery theory initiated, forty years ago, by Wu on his seminal paper [17, “On the decision problem and the mechanization of theorem-proving in elementary geometry”], based in computational (complex) algebraic geometry. This theory has evolved, along the years, yielding a variety of methods that have been recognized to be a quite successful approach to automated reasoning in elementary geometry, as already shown, long ago, by the quantity and quality of the performing examples in [6]. In this paper, we will follow the protocol and notation described in [7, Chapter 6, Section 4], quite similar to that of [8, 15] or [18]. Its recent implementation (see [1]) in a free mathematics software, with millions of users worldwide, brings again to the frontline some pending issues.

The point we will address in this paper deals with the most convenient way(s) of handling hypotheses and theses that describe negative assertions, such as “consider two different points” (i.e., two points that are not equal), or “let A, B, C be the vertices of a non-degenerate triangle” (i.e., three points that A, B, C neither coincide nor lie on a line), etc. The relevance of clarifying this issue is not just restricted to extending the mechanical proving method to handle a larger kind of statements. In fact, as we will show in the next Sect. 1 of this paper, non-degeneracy conditions arise in a natural way along with the traditional protocol for theorem proving of purely affirmative statements.

It happens that, in order to introduce, as input for the standard algebraic geometry algorithms, the requirement to avoid such degeneracies, the given polynomial inequalities $p_1(x_1, \dots , x_n) \ne 0$ must be expressed by means of equations. In the tradition¹ of automated theorem proving this conversion has been achieved through two possible approaches, that we will describe in detail in Sect. 2: Rabinowitsch’s trick and ideal saturation.

Rabinowitsch’s trick is an old companion to automated proving in geometry [10], where it has been used to formulate negations of equalities, the so-called “disequality” relations. Despite its antiquity, the current validity and interest of this approach can be confirmed, for example, by considering the recent research of Kapur et al. [11] on a generalization of the “trick”. See also [3, Example 6.1] for a sound, abstract, description of this trick, i.e., the replacement of a locally closed set $A {\setminus } B$, where A, B are algebraic subsets of an affine space $K^n$, by an algebraic set in $K^{n+1}$, the so-called “Rabinowitsch cover”, such that the set-theoretic projection of the cover is exactly the locally closed set and, thus, the closure—in the Zariski topology—of the projection of the cover can be computed through elimination.

On the other hand, ideal saturation is a direct algebraic way to compute $\overline{A {\setminus } B}$ without requiring to replace the locally closed set $A {\setminus } B$ by an algebraic set on a higher dimensional affine space and then projecting it down to $K^n$. Its relation to Rabinowitsch’s trick is well known in Commutative Algebra, and the potential impact of using saturation as an alternative to Rabinowitsch’s trick for theorem proving has been already highlighted in [8, Section 5], but it seems a detailed and general analysis of the pros and cons of both approaches, regarding their faithfulness as translations of negative statements, has never been thoroughly addressed.

Thus, the main contribution of this paper is to study, in detail, the different implications of adopting each of these formulations for describing negative theses and hypotheses. Section 3 focuses on the consequences of both methods for stating negative theses, suggesting that saturation could be considered as more reliable in this context (see Proposition 5), while Sect. 4 deals with the introduction of negative hypotheses, clarifying—see Theorems 1 and 2— the different, albeit close, results in each of the two alternate proposals. Section 5 discusses in detail an example, showing the computational pros and cons of both approaches. Finally, Sect. 6 establishes some conclusions for the future consideration of automatic theorem proving software developers.

For simplicity of notation, in this paper, we will denote by H (resp. T) the collection of polynomials involved in the hypotheses (resp. theses) and the ideal generated by them.

2 A short digest on automatic proving and discovery by algebraic geometry methods

Roughly speaking, the computational algebraic geometry theorem proving method proceeds by assigning coordinates and equations to the elements (points, lines, circles, etc.) and conditions (perpendicularity, incidence, etc.) of the involved geometric hypotheses H and theses T. In this way the geometric statement, which we will symbolize as $H \Longrightarrow T$, is translated as an inclusion $V(H) \subseteq V(T)$ between the solution set, V(H), of the system of equations $\{H=0\}$ and that, V(T), of the set of equations $\{T=0\}$. Finally, this inclusion needs to be tested by some computational algebraic geometry methods.

Over an algebraically closed field K—an assumption we will keep along the paper—, one practical protocol to perform this test is the refutational approach introduced by Kapur [10], in which testing the inclusion $V(H) \subseteq V(T)$ turns to deciding if $V(H) {\setminus } V( T)$ is empty or not. This is, obviously, equivalent to showing that its Zariski-closure $\overline{V(H) {\setminus } V( T)}$ is empty or not. But this fact can be checked by testing the emptiness of the corresponding Rabinowitsch cover (i.e., by determining the membership of 1 in the defining ideal of the cover) since the projection of an algebraic set is empty if and only if the set is empty. In fact, when T is a single thesis—we will assume this fact in what follows, as it is straightforward to adapt all the obtained results to the general case—verifying that $H \wedge \lnot T$ is empty is equivalent, by the Weak Nullstellensatz, to simply checking if $1 \in H^e + (T\cdot t-1)$, where $H^e$ is the extension of H to the polynomial ring with an extra variable t.

As it is well known, the reduction from the Strong to the Weak Nullstellensatz, by introducing $T\cdot t-1=0$ as the algebraic, affirmative formulation for $\lnot \{T=0\}$ is, precisely, the role of the so-called Rabinowitsch’s trick, see  [14]. In summary, there is a special, and since long, relation between automatic proving in geometry and this particular trick.

Going a little bit further, let us remark that, in the algebraic geometry approach to automated theorem proving, it happens that in most cases we are not actually dealing with proving, but with discovering! Indeed, many statements that seem obviously true to human intuition, turn out to be false in the algebraic formulation, in the sense of not fully verifying $V(H) \subseteq V(T)$. Thus, the main task for the automatic reasoning theory turns out to be devising algorithms to find out extra hypotheses that will constrain the set V(H) in order to fit inside V(T): i.e., to discover how to modify a given statement so that it becomes true! See [16] for a thorough reflection and bibliographic references on this involved issue.

A key ingredient in this framework is the concept of set of independent variables modulo the hypotheses ideal, i.e., a set of variables such that no polynomial, in these variables alone, belongs to the ideal H. Examples of sets of free variables are the collection of three times two coordinates describing the vertices of an arbitrary triangle, or only one of the coordinates of a point constrained to be in a circle, etc.

Among the many different sets of independent variables for a particular hypotheses ideal, we will consider sets of maximum cardinality: in this way, the remaining variables will verify some algebraic dependence over the independent ones and thus—except at some special cases—they are finitely determined for each setting of the independent variables. Therefore, it is exclusively in terms of the independent variables that we will consider reasonable to formulate the extra hypotheses needed to modify some given geometric statement, to turn it strictly true.

Obviously, it is crucial to automatically find such conditions: this can be done, roughly speaking, by elimination of the extra variable t and the non-independent variables (say, $x_{s+1},\dots ,x_n$) in the ideal $H^e + (T\cdot t-1)$. Indeed, the zero set of $H^e + (T\cdot t-1)$ exactly corresponds to the “failure cases” where H and $\lnot \ T$ simultaneously hold.

Thus, by adding to the given hypotheses H the negation of any of the polynomials in the elimination ideal of $H^e + (T\cdot t-1)$, we will get a true statement. These additional, negative hypotheses (such as these two given points must be truly different, the given triangle should not collapse to a line, etc.) expressed in terms of the independent variables, are known as non-degeneracy conditions.

Of course, it can happen that the elimination of t and the dependent variables in the ideal $H^e + (T\cdot t-1)$ is just the zero ideal and, in this case, the only non-degeneracy condition turns out to be $0\ne 0$, so that it does not hold over any instance of the geometric hypotheses. Notice that this zero-ideal case is the only possibility for getting an empty hypotheses statement when adding the negation of an equation $h'=0$, where $h'$ arises from the elimination of $H^e + (T\cdot t-1)$ in terms of independent variables. Thus, the name generally true is reserved to statements where this elimination ideal $\big (H^e + (T\cdot t-1)\big )\cap K[x_1,\dots ,x_s]$ is not zero; logically, the name non generally true is applied to those statements in which the former ideal is zero (that is, generally true is false). Note that we are employing the terminology of [6] and some recent papers as [1, 8, 15], but recall that in some classic references as [7] or [12] these statements are called generically true and non generically true, respectively.

When the elimination ideal is zero, it is advisable to consider, instead, the elimination of the same dependent variables, but now in the ideal of hypotheses and thesis $H+T$. If this elimination is not zero, the given statement is labeled as generally false (and non generally false if it is zero).

Obviously, when the elimination of the dependent variables in $H+T$ is not zero, adding as complementary, affirmative hypotheses the equations of a basis of this elimination ideal we are led to a new statement, and we should restart again our protocol.

Notice that the new hypotheses variety could be empty if and only if $H+T=(1)$, i.e., if the elimination ideal turns out to be (1), and from there we can conclude the truth of whatever statement. It is the extremely false case, in which the hypothesis variety has nothing in common with the thesis variety. Our approach does not disregard this option; but routinely checking that the analyzed statements have a non empty hypotheses set should be included in any theorem proving algorithm, in order to detect trivialities.

On the other hand, if the elimination in $H+T$ yields zero, we are in the non generally false and non generally true case. See [7, Chapter 6, Section 4] or [8, 15] for further details on the whole algorithm.

Thus, the general automatic proving procedure ends, either with a generally true statement (after discovering some new, affirmative and/or negative conditions), or arriving at a neither generally false nor generally true situation, a quite challenging context, yielding as well to the discovery of new statements, but in a more involved way. See [5, 18] for some recent advances concerning this last issue.

3 Introducing negative conditions: different ways...

Summarizing, negative conditions appear naturally in classical automated theorem proving in two different circumstances:

• to refute the thesis T, in order to establish if the given statement is generally true or not;

• if generally true, to add, as complementary, negative hypotheses, some newly discovered non-degeneracy conditions.

On the other hand, the high complexity of the polynomial Gröbner basis algorithms involved in the method explained before [7] compels the user to manually introduce, before starting to run the proving algorithm, some easy-to-guess non-degeneracy conditions, to attempt to simplify the computation.

Bearing this in mind, we think that the second item above should be extended and reformulated as follows:

• to add, at different stages of the proving protocol, as complementary hypotheses, human or automatically guessed non-degeneracy conditions.

Thus, an important task is to find ways to introduce both the refutation of a thesis and non-degeneracy conditions, so that it reflects (as closely as possible) the geometric meaning of the added condition (i.e., to avoid some degenerate cases, to negate some theses) and expresses it by means of equations.

As mentioned above, traditionally (at least since [10]) the negation of a given geometric property described by the equation $f=0$, is handled as an equation by adding some auxiliary variable t and considering the equation $f \cdot t-1=0$ as representing $\lnot \{f=0\}$, emulating Rabinowitsch’s trick. It is easy to generalize this approach to refutation for the case of having to negate the conjunction or the disjunction of several conditions, see [8, Appendix].

However, the avoidance of some condition $f=0$ can be expressed considering the Zariski closure of the difference $V(H) {\setminus } V(f)$, i.e., by considering as new hypotheses the polynomial equations expressing the smallest set that verifies the given hypotheses and not the condition $f=0$. In general, if I, J are ideals of a polynomial ring $K[x_1,\dots ,x_n]$, the saturation of I by J is defined as $\texttt {Sat}(I,J)=I:J^\infty = \cup _{n} (I:J^n)$ (see [7, 8]), where $I:J=\{g\in K[x_1,\dots ,x_n] :gJ\subseteq I\}$, and it satisfies $V(\texttt {Sat}(I,J))=\overline{V(I){\setminus } V(J)}$. When the ideal J is principal, $J=(j)$, we merely denote $\texttt {Sat}(I,j)$.

In summary, the other option we are considering here to include non-degeneracy conditions $\lnot \{f=0\}$ is to saturate the ideal of hypotheses by the ideal $J=(f)$. Again, it is straightforward the generalization of this idea of saturation to the case of several conditions (see [8, Appendix]). As mentioned in the previous section, we could say that saturation is a direct way to compute $V(H) {\setminus } V(f)$ without requiring adding one extra variable and then eliminating it.

This second option could seem, at first glance, more sophisticated than the first one—the implementation of Rabinowitsch’s trick. But there is not a big difference. In fact, [8, Proposition 6 and Corollary 2 of Appendix] shows that the saturation of the ideal I by another ideal $J=\prod _{i=1}^{r} J_i$, where $J_i=(f_{i1},\dots ,f_{il_i})$, satisfies:

$$\begin{aligned} \texttt {Sat}(I,J)&= \Big (I^e+\big ((f_{11} \cdot t_1-1)\cdots (f_{1l_1}\cdot t_1-1),\dots ,(f_{r1} \cdot t_r-1)\cdots (f_{rl_r}\cdot t_r-1)\big )\Big ) \\&\quad \cap K[x_1,\dots ,x_n]; \end{aligned}$$

in particular, it holds² that

$$\begin{aligned} \texttt {Sat}(I,f)=\big (I^e+(f \cdot t-1)\big )\cap K[x_1,\dots ,x_n], \end{aligned}$$

(1)

as it is stated in [7, Theorem 14 of Chapter 4, Section 4].

Thus, the actual dilemma is: do we want to add non-degeneracy conditions as in Rabinowitsch’s trick, by carrying around within H an extra, alien variable, which should be eliminated at the end of the theorem proving or discovery process—i.e., when considering the ideal $H^e+(T \cdot t-1)$; or should we deal, from the beginning, with the non degeneracy conditions expressed in terms of the “given” variables of our statement, by saturation? And, actually, does it imply any difference concerning theorem proving?

This dilemma does not seem to appear concerning the use of Rabinowitsch’s trick or saturation in order to determine if a theorem is generally true by refuting the thesis. It is easy to prove that both approaches yield the same result: it follows from (1) and the fact that

$$\begin{aligned} \Big (H^{e}+(T\cdot t-1)\Big )\cap K[x_1,\dots ,x_s]= \Big (H^{e}+(T\cdot t-1)\Big )\cap K[x_1,\dots ,x_n]\cap K[x_1,\dots ,x_s]. \end{aligned}$$

4 ...different consequences: introducing negative theses

In this section, we will analyze the different behavior of both approaches (Rabinowitsch, saturation) regarding the introduction of negative theses. Note that this task is not as important as the introduction of negative hypotheses (which will be tackled in the following section), because the former just enlarges the realm of classical automated theorem proving, while the latter appears naturally on it.

Example 1

Let us consider the following quite artificial statement: given a general triangle, with free vertices $A(0, 0), B(1,0), C(c_1,c_2)$, we assert that $c_2 \ne 0$, i.e., that C does not lie in the AB line. Intuitively this statement seems generally true. We consider the ideal $H =(0)$ as the zero ideal, since there are no hypotheses; moreover, both variables, $c_1, c_2$ are free.

Then, we apply the protocol and start computing $H+(T\cdot t-1)$, with $T := \{c_2 \ne 0\}$. Using Rabinowitsch’s trick we should consider $T := \{c_2\cdot z-1=0\}$, with an auxiliary variable z, and then proceed to compute the elimination of the variables z and t in the ideal $H+\big ((c_2\cdot z-1)\cdot t-1\big )=(0)+\big ((c_2\cdot z-1)\cdot t-1\big )=\big ((c_2\cdot z-1)\cdot t-1\big )$. The obvious result is (0), so the statement is non generally true and we should proceed by considering the ideal $H+T$, i.e., $(0)+(c_2\cdot z-1)$ and eliminating the variable z here. The result is, again, zero. So we are stuck in the non generally true and non generally false case!

On the other hand, if we model the thesis T as the saturation of $H=(0)$ by $c_2$ we get $\texttt {Sat} ((0),(c_2))=(0)$, so the thesis should be considered to be $T=0$ and, then, we start checking if this thesis is generally true, but computing the ideal $H+(T\cdot t-1)$, i.e., ideal $(0)+(1)=(1)$. We get that the statement is not only generally but always true, since the only non-degeneracy condition is $1 \ne 0$ !

As we can see in the above example, we can obtain quite different results following both methods. But this is not just a particular behavior in some cases. In general, we can state the following unexpected facts:

Proposition 1

The introduction of a negative thesis $T_1 := \{p\ne 0\}$ by using Rabinowitsch’s trick, always yields a non generally true statement $H \Longrightarrow T_1$.

Proof

Let us assume that $\{x_1,\dots ,x_s\}$ are the independent variables for H. Then let us prove that the closure of the projection over this affine space, of the variety $V(H) \cap V((p\cdot z-1)\cdot t-1)$ lying in the space of the variables $\{x_1,\dots ,x_s, x_{s+1},\dots , x_n,z,t\}$, is the whole $\{x_1,\dots ,x_s\}$-space. In fact, take any point $(x_1,\dots ,x_s)$ in the projection of V(H), which is, by definition of independent variables, dense in the affine space, and we will prove that it is also in the projection of $V(H) \cap V\big ((p\cdot z-1)\cdot t-1\big )$.

First we notice that, because $(x_1,\dots ,x_s)$ lies in the projection of V(H), there are values of $x_{s+1},\dots , x_n$ such that $(x_1,\dots ,x_s, x_{s+1},\dots , x_n)$ is in V(H). If, for one of these points in V(H), it happens that $p(x_1,\dots , x_n)=0$, then by taking $t=-1$ and an arbitrary value of z, we will have that the point $(x_1,\dots , x_n,z,-1)$ is in $V(H) \cap V\big ((p\cdot z-1)\cdot t-1\big )$. On the other hand, if $p(x_1,\dots , x_n)\ne 0$, we consider a value of $z \ne 1/p(x_1,\dots , x_n)$, so that $p\cdot z-1 \ne 0$. Finally, by taking $t=1/(p\cdot z-1)$, we will have, again, that the point $\big (x_1,\dots , x_n,z,1/(p\cdot z-1)\big )$ is in $V(H) \cap V\big ((p\cdot z-1)\cdot t-1\big )$.

This surprising result could suggest the idea that this method fails to model geometric problems with negative thesis. Indeed, an intuitive approximation might consider that the two successive negations involved here (one, for the negative thesis; two, for the refutational approach required for checking generally true statements), would be equivalent to simply verifying the thesis in an affirmative way. That is, common sense is prone to conclude that verifying if a negative thesis (introduced through Rabinowitsch’s trick) is generally true would be equivalent to verifying if the corresponding affirmative thesis is generally false, but see some of the examples and propositions below. In fact, postponing the elimination of z until the end of the process, which is the essence of Rabinowitsch’s trick, forces us to consider the formulation of the negative thesis $p\cdot z-1$ just as a simple statement in $K[x_1,\dots , x_n,z]$, rather than the negation of something, yet with subtle relations with the corresponding affirmative statement.

Notice that, in general, we have [5, Proposition 2.3]:

Proposition 2

A statement $H \Longrightarrow T$ cannot be simultaneously generally true and generally false, that is, it cannot happen that both $H+T$ and $H^{e}+ (T\cdot t-1)$ have, at the same time, some non-zero polynomials in the independent variables alone.

On the other hand, it is easy to notice that, by applying directly the definitions, we have:

Proposition 3

If a statement with an affirmative thesis $T_2 := \{p = 0\}$ is generally true, then the same statement but with the negative thesis (formulated through Rabinowitsch’s trick) $T_1 := \{p\ne 0\}$ will be generally false, and conversely.

Putting together the two precedent propositions, it follows immediately the following result:

Proposition 4

If a statement with an affirmative thesis $T_2 := \{p = 0\}$ is generally false, then the same statement, but with the corresponding negative thesis (formulated through Rabinowitsch’s trick) $T_1 := \{p\ne 0\}$ will be non generally false.

Proof

If a statement with an affirmative thesis $T_2 := \{p = 0\}$ is generally false, then Proposition 2 says that it cannot be generally true and thus, by Proposition 3, the corresponding negative thesis (formulated through Rabinowitsch’s trick) $T_1 := \{p\ne 0\}$ will be non generally false. $\square$

Corollary 1

In summary: if $H \Longrightarrow T_2$ is generally false, then necessarily

• $H \Longrightarrow T_2$ is non generally true;

• $H \Longrightarrow T_1$ is non generally false and non generally true.

On the other hand, if $H \Longrightarrow T_2$ is non generally false, then, there are two options: if $H \Longrightarrow T_2$ is also generally true, we will have that $H \Longrightarrow T_1$ is generally false as well, and non generally true; and if $H \Longrightarrow T_2$ is non generally false and non generally true, then $H \Longrightarrow T_1$ is also non generally false and non generally true.

Example 2

If we consider $H:=\{(y-1)\cdot (y-2)=0\}$ in the variables $\{x,y\}$, with x the only independent variable, and $T_2:=\{y-1=0\}$, $T_1:=\{(y-1)\cdot z-1=0\}$ it is easy to check that $H \Longrightarrow T_2$ is both non generally true and non generally false, and the same happens for $H \Longrightarrow T_1$. On the other hand, if we take $T_2:=\{y-3=0\}$, $T_1:=\{(y-3)\cdot z-1=0\}$, we obtain that $H \Longrightarrow T_2$ is non generally true, but generally false, while $H \Longrightarrow T_1$ is both non generally true and non generally false. Finally, if we take $H:=\{(y-1)=0\}$ in the variables $\{x,y\}$, and $T_2:=\{y-1=0\}$, $T_1:=\{(y-1)\cdot z-1=0\}$ it is easy to check that $H \Longrightarrow T_2$ is generally true, but non generally false, while $H \Longrightarrow T_1$ will be no generally true, but generally false. This covers all possibilities.

Similarly to Proposition 3, for the formulation of negative thesis using saturation, we have the following:

Proposition 5

If the statement $H \Longrightarrow T_2$ is generally true then the statement $H \Longrightarrow T_1$, formulated by introducing the negative thesis $T_1 := \{p\ne 0\}$ by using saturation, is generally false. Analogously, if $H \Longrightarrow T_2$ is generally false then the statement $H \Longrightarrow T_1$, formulated by introducing the negative thesis $T_1 := \{p\ne 0\}$ by using saturation, is a generally true statement.

Proof

If $H \Longrightarrow T_2$ is generally true, it means that the elimination of dependent variables modulo H in $H^{e} +(p\cdot t-1)$ is not zero. Let J be this elimination ideal. Now, $H \Longrightarrow T_1:=\{\texttt {Sat} (H, p)\}$, expressed by saturation, is generally false because if we eliminate the dependent variables in $H + T_1$ we get $(H+\texttt {Sat} (H, p))\cap K[x_1,\dots ,x_s]=(H+((H^{e} +(p\cdot t-1))\cap K[x_1,\dots ,x_n]))\cap K[x_1,\dots ,x_s]$, where the inner intersection just means the elimination of t. Obviously, this intersection contains J, which is already an ideal in the independent variables, so this inclusion is not affected by adding H or by the outer intersection, hence $(H+\texttt {Sat} (H, p))\cap K[x_1,\dots ,x_s]=(H+((H^{e} +(p\cdot t-1))\cap K[x_1,\dots ,x_n]))\cap K[x_1,\dots ,x_s] \supseteq J\ne (0)$.

Concerning the second statement in this proposition, let us assume that $\texttt {Sat}(H,p)$ is principal, for simplicity; say, generated by q. Then there is a power of p, such as $p^r$, verifying that $q\cdot p^r \in H$. Next, notice that if $H+(p)$ has some polynomial in the independent variables (i.e., if $H \Longrightarrow T_2$ is generally false), then the same happens for $H+(p^n)$, for whatever power of p; thus, the elimination of the independent variables in $H+(p^r)$ will also be not zero. On the other hand, we observe that $p^r$ is in $H^{e} + \big (\texttt {Sat}(H,p) \cdot t-1\big )$, since equality (1) tells us that the elimination of t in this ideal is $\texttt {Sat} \big (H, \texttt {Sat}(H,p)\big )$, and $p^r\cdot q \in H$. Thus, $H^{e} + \big (\texttt {Sat}(H,p) \cdot t-1\big ) \supseteq H+(p^r)$ and it follows the corresponding elimination is not zero. $\square$

Example 3

If we consider $H:=\{(y-1)\cdot (y-2)=0\}$ in the variables $\{x,y\}$, with x the only independent variable, and $T_2:=\{y-1=0\}$, $T_1:=\texttt {Sat} (((y-1)\cdot (y-2)), (y-1))$=$\{y-2=0\}$ it is easy to check that $H \Longrightarrow T_2$ is both non generally true and non generally false, and the same happens for $H \Longrightarrow T_1$. On the other hand, if we take $T_2:=\{y-3=0\}$, $T_1:=\texttt {Sat} (((y-1)\cdot (y-2)), (y-3))$=$\{(y-1)\cdot (y-2)=0\}$, we obtain that $H \Longrightarrow T_2$ is non generally true, but generally false, while $H \Longrightarrow T_1$ is generally true and non generally false. Finally, if we take $H:=\{(y-1)=0\}$ in the variables $\{x,y\}$, and $T_2:=\{y-1=0\}$, $T_1:=\texttt {Sat} ((y-1), (y-1))=(1)$ it is easy to check that $H \Longrightarrow T_2$ is generally true, but non generally false, while $H \Longrightarrow T_1$ will be non generally true, but generally false. We see, comparing with Example 2, that when $H \Longrightarrow T_2$ is generally false, the behavior with saturation is diverse from the one with Rabinowitsch.

5 ...different consequences: introducing negative hypotheses

In [8, Example 6 of Section 5] it is presented one specific example showing how both methods (Rabinowitsch, saturation) differ in a common context, yielding, if a non-degeneracy hypothesis is introduced using Rabinowitsch’s trick, an interesting theorem discovering the conditions for the orthic triangle of a given triangle with non-collinear vertices to be equilateral. On the other hand, if the non-collinearity of the vertices is introduced by saturation, there is no discovery at all. Although the concept of theorem discovery in [8] and the one from [15] we have just recalled here in the introduction (which has been recently implemented in some popular mathematical software [1, 2]) are practically the same, the framework is a little bit different: in [8] the approach is slightly more sophisticated.

In order to analyze the behavior of both approaches to non-degeneracy hypotheses, let us denote:

$$\begin{aligned} H_1&:= H^e+(f \cdot t-1),\\ H_2&:= \texttt {Sat} (H, f). \end{aligned}$$

Thus, $H_1, H_2$ are the enlarged ideals of hypotheses, corresponding to the two possibilities of introducing non-degeneracy conditions such as $f\ne 0$ over an ideal of hypotheses H of a given statement.

Remark 1

With the above notation, it holds that $H_2^e \subseteq H_1$, since the saturation is equal to the elimination of the variable t in the ideal on the right side (i.e., the contraction into the ring $K[x_1,\dots ,x_n]$), and the contraction and, then, extension of an ideal, is always contained in the given ideal.

Example 4

The following trivial example $H=(0)$, $f=x$, shows that, in general, the inclusion $H_2^e\subset H_1$ is strict. We find that $H_2=\texttt {Sat} (H, f)=(0)$, its extension is, again, (0) and $H_1=H^e+(f \cdot t-1)= (x\cdot t-1)$. In this case, the saturation does not assimilate the information contained in $x\ne 0$: the zero set of $\texttt {Sat} (H, f)$ includes the points where $x=0$, although we wanted to avoid such instances. This situation is due to the early consideration of the closure in the saturation method.

Taking Remark 1 into account, we are ready to present the following basic result.

Proposition 6

Notation as above. The set of hypotheses $H_1$ provides, in general, more additional conditions for discovery that the set $H_2$; that is:

$$\begin{aligned} (H_2 + T)\cap K[x_1,\dots ,x_s] \subseteq (H_1 + T) \cap K[x_1,\dots ,x_s]. \end{aligned}$$

(2)

Proof

Using the properties of extension and contraction of ideals, it is clear that $H_2+T\subseteq (H_2+T)^{ec}=(H_2^e+T)^c$, where $(-)^c$ symbolizes the contraction of the ideals to the ring $K[x_1,\dots ,x_n]$. By Remark 1, we can state that $(H_2^e+T)^c \subseteq (H_1+T)^c$. Thus, intersecting both $H_2+T$ and $(H_1+T)^c$ with $K[x_1,\dots ,x_s]$, the inclusion (2) holds. $\square$

Corollary 2

It follows that if the statement $H_2 \Longrightarrow T$ is generally false, $H_1 \Longrightarrow T$ will also be generally false. Replacing in the proposition above the polynomial T with $T\cdot t'-1$, we obtain the same inclusion and, thus $H_2 \Longrightarrow T$ generally true implies that $H_1 \Longrightarrow T$ is, as well, generally true.

Example 5

Again, we present a simple example to illustrate that the inclusion in (2) is, in general, strict. Let us retake the previous Example 4, with thesis $T= (x)$ (essentially, the same example which appears at the beginning of [8, Section 5]). Clearly, the variable x is independent. Recall that $H_1=(x\cdot t-1)$ and $H_2=(0)$. If we add T to our ideals and eliminate all variables except x (i.e., the variable t), we obtain, respectively, the sets (1) and (x). It is clear that adding the condition $1=0$ to the hypotheses set makes the hypotheses variety empty, from which we could conclude whatever we wanted. So, this is not an interesting option. But neither is the set obtained from saturation, because it leads to a contradiction with $x\ne 0$.

So, the previous example ends up in a discovery, but not in a proper one.

In order to gain a better understanding of discovery from each one of the approaches, we will now precise the difference between the two sets of derived additional conditions (a result which is similar to [8, Proposition 3]). Remark that we just consider the case in which the non-degeneracy condition introduced by the user is formulated in terms of the independent variables; a reasonable restriction, since these variables are the only ones we can freely manipulate.

Lemma 1

Notation as above. Assume that $f \in K[x_1,\dots ,x_s]$. Then it holds that:

$$\begin{aligned} (H_2 + T)\cap K[x_1,\dots ,x_s]&= (H_1 + T) \cap K[x_1,\dots ,x_s]\\&\!\!\iff (H_2 + T)\cap K[x_1,\dots ,x_s]\\&=\texttt {Sat} \big ((H_2 + T)\cap K[x_1,\dots ,x_s],f\big ). \end{aligned}$$

Proof

The statement immediately follows if we prove the equality

$$\begin{aligned} \big (H^{e}+(f\cdot t-1)+T\big )\cap K[x_1,\dots ,x_s]=\texttt {Sat}\Big (\big (\texttt {Sat}(H,f)+T\big ) \cap K[x_1,\dots ,x_s],f\Big ), \end{aligned}$$

(3)

stating that the additional conditions for discovery found employing Rabinowitsch’s trick are the saturation of those provided by the saturation method.

First of all, we recall that, by equality (1), it holds that $\big (H^{e}+(f\cdot t-1)+T\big )\cap K[x_1,\dots ,x_n]=\texttt {Sat}(H+T,f)$. Let us continue proving that the right side of this equality can be regarded as follows

$$\begin{aligned} \texttt {Sat}(H+T,f)=\texttt {Sat}\big (\texttt {Sat}(H,f)+T,f\big ). \end{aligned}$$

(4)

It is clear that $\texttt {Sat}(H+T,f)\subseteq \texttt {Sat}\big (\texttt {Sat}(H,f)+T,f\big )$, since always $H\subseteq \texttt {Sat}(H,f)$. Conversely, if $g\in \texttt {Sat}(\texttt {Sat}(H,f)+T,f)$, there exists $n\in \mathbb {N}_{>0}$ such that $g\cdot f^n=a+b$, with $a\in \texttt {Sat}(H,f)$ and $b\in T$. Again, there exists $m\in \mathbb {N}_{>0}$ such that $a\cdot f^m\in H$; so, $g\cdot f^{n+m}=a\cdot f^m + b\cdot f^m\in H+T$. Thus, it follows by definition that $g\in \texttt {Sat}(H+T,f)$.

Now, in order to end proving the initial equality (3) it remains to exhibit that

$$\begin{aligned}&\texttt {Sat}\big (\texttt {Sat}(H,f)+T,f\big )\cap K[x_1,\dots ,x_s]\\ {}&\quad =\texttt {Sat}\Big (\big (\texttt {Sat}(H,f)+T\big )\cap K[x_1,\dots ,x_s],f\Big ). \end{aligned}$$

Let $g\in \texttt {Sat}\big (\texttt {Sat}(H,f)+T,f\big )\cap K[x_1,\dots ,x_s]$. It is clear that $g\cdot f^n\in \texttt {Sat}(H,f)+T$ for some $n\in \mathbb {N}_{>0}$. Both g and $f^n$ belong to $K[x_1,\dots ,x_s]$, whence $g\cdot f^n$ belongs to the same ring, too. So, $g\in \texttt {Sat}\Big (\big (\texttt {Sat}(H,f)+T\big )\cap K[x_1,\dots ,x_s],f\Big )$. The converse follows trivially from the fact that both $\big (\texttt {Sat}(H,f)+T\big )\cap K[x_1,\dots ,x_s]$ and (f) lie on $K[x_1,\dots ,x_s]$. $\square$

The previous lemma allows us to conclude the following result.

Theorem 1

The statement $H_1\Longrightarrow T$ is generally false if and only if the statement $H_2\Longrightarrow T$ is also generally false; analogously, $H_1\Longrightarrow T$ generally true is equivalent to $H_2\Longrightarrow T$ generally true.

Proof

The first assertion follows from Lemma 1 and the fact that an ideal is zero if and only if its saturation by another, non-zero, arbitrary ideal, is zero. For the second one, it suffices to replace the ideal T in Lemma 1 with $T\cdot t'-1$ and to reason as above. $\square$

Theorem 1 says that the method employed for introducing the non-degeneracy conditions does not affect whether the theorem is generally true or generally false, but it can provide different sets of additional hypotheses for discovery (see Example 5). Henceforth, we will denote them by:

$$\begin{aligned} \mathcal {H}_1&:= (H_1+T)\cap K[x_1,\dots ,x_s],\\ \mathcal {H}_2&:= (H_2+T)\cap K[x_1,\dots ,x_s]. \end{aligned}$$

Recall (see Eq. (3)) that $\mathcal {H}_1=\texttt {Sat}(\mathcal {H}_2,f)$. Following the traditional protocol for discovery, the next step would be to consider the statements:

$$\begin{aligned}&St_A:\quad H_1+\mathcal {H}_1^e\Longrightarrow T,\\&St_B:\quad H_2+\mathcal {H}_2^e\Longrightarrow T, \end{aligned}$$

and continue to check out whether the new theorems are generally true or not. But we have already seen in Example 5 that $\mathcal {H}_2$ may be generated by elements contradicting the negation $\lnot \{f= 0\}$. Therefore, it might be interesting to saturate again $H_2+\mathcal {H}_2^e$ by f and to change $St_B$ by

$$\begin{aligned} St_{B'}:\quad \texttt {Sat}(H_2+\mathcal {H}_2^e,f)\Longrightarrow T, \end{aligned}$$

where $\texttt {Sat}(H_2+\mathcal {H}_2^e,f)=\texttt {Sat}(H+\mathcal {H}_2^e,f)$ (it follows from repeating the proof of equality (4)). Note that, also, $H_1+\mathcal {H}_1^e=H^{e} +\mathcal {H}_1^e+(f\cdot t-1)$. Finally, and with the goal of generalizing as well as making easier the proof of the following results, we will consider

$$\begin{aligned}&St_1:\quad H^{e}+\mathcal {H}_1^e+(f\cdot t-1)\Longrightarrow T,\\&St_2:\quad H^{e}+\mathcal {H}_2^e+(f\cdot t-1)\Longrightarrow T,\\&St_3:\quad \texttt {Sat}(H+\mathcal {H}_1^e,f)\Longrightarrow T,\\&St_4:\quad \texttt {Sat}(H+\mathcal {H}_2^e,f)\Longrightarrow T, \end{aligned}$$

being $St_1=St_A$ and $St_4=St_{B'}$.

Recall that, by enlarging the set of hypotheses H with $\mathcal {H}_1^e$ or $\mathcal {H}_2^e$, some of the independent variables $\{x_1,\dots ,x_s\}$ ruling the initial theorem $H\Longrightarrow T$, could become dependent. In that case we would have to deal with two new sets of independent variables: $\varLambda _1:=\{x_1,\dots ,x_{s_1}\}$, the independent variables in $H+\mathcal {H}_1^e$, as well as $\varLambda _2:=\{x_1,\dots ,x_{s_2}\}$ for $H+\mathcal {H}_2^e$. Since the inclusion $H_2^e\subseteq H_1$ holds, it follows that $\varLambda _1\subseteq \varLambda _2$.

Nevertheless, we will avoid such subtleties by restricting, in what follows, to the case in which f is formulated just in terms of the variables in $\varLambda _1$: f “as independent as possible”.

Aiming to establish the relationships among the statements $St_1$, $St_2$, $St_3$ and $St_4$, we present the following useful lemma.

Lemma 2

With the above notation, it holds that

$$\begin{aligned} \texttt {Sat} \Big (H+\mathcal {H}_1^e,f\Big )=\texttt {Sat} \Big (H+\mathcal {H}_2^e,f\Big ). \end{aligned}$$

(5)

In addition,

$$\begin{aligned}&\Big (H^e+\mathcal {H}_1^e+(f\cdot t -1)+(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_n,t']\nonumber \\&\quad =\Big (H^e+\mathcal {H}_2^e+(f\cdot t -1)+(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_n,t']. \end{aligned}$$

(6)

Proof

We infer from Lemma 1 that

$$\begin{aligned} \texttt {Sat}\Big (H+\mathcal {H}_1^e,f\Big )=\texttt {Sat}\Big (H+\texttt {Sat}(\mathcal {H}_2,f)^e,f\Big ), \end{aligned}$$

being the term in the right side equal to $\texttt {Sat}\big (H+\texttt {Sat}(\mathcal {H}_2^e,f),f\big )$ (see [8, Appendix]). From here, it suffices to essentially repeat the proof of equality (4) to have equation (5) proved: the two sets of additional hypotheses $\mathcal {H}_1$ and $\mathcal {H}_2$ yield the same ideal when added to H and saturated by f.

As for (6), employing equality (1) we see that both $\big (H^e+\mathcal {H}_1^e+(f\cdot t -1)+(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_n,t']=\texttt {Sat}\big (H^e+\mathcal {H}_1^e+(T\cdot t'-1),f\big )$ and $\big (H^e+\mathcal {H}_2^e+(f\cdot t -1)+(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_n,t']=\texttt {Sat}\big (H^e+\mathcal {H}_2^e+(T\cdot t'-1),f\big )$ hold. Again, Lemma 1 and the idea lying under equality (4) enable us to state:

$$\begin{aligned}&\texttt {Sat}\big (H^e+\mathcal {H}_1^e+(T\cdot t'-1),f\big )\\&\quad =\texttt {Sat}\big (H^e+\texttt {Sat}(\mathcal {H}_2,f)^e+(T\cdot t'-1),f\big )\\&\quad =\texttt {Sat}\big (H^e+\texttt {Sat}(\mathcal {H}_2^e,f)+(T\cdot t'-1),f\big )\\&\quad =\texttt {Sat}\big (H^e+\mathcal {H}_2^e+(T\cdot t'-1),f\big ), \end{aligned}$$

and we are done. $\square$

Remark 2

Note that the only requirement for Lemma 2 to hold is that $f\in K[x_1,\dots ,x_s]$, since this is an essential hypotheses in Lemma 1.

Now, we are ready to state our main results.

Theorem 2

Notation as above. The statements $St_1,\,St_2,\,St_3\ \text {and}\ St_4$ are generally true if and only if one of them is generally true. Furthermore, $St_3$ and $St_4$ have exactly the same hypotheses, and the non-degeneracy conditions of $St_1$ are equal to those of $St_2$ provided that $\varLambda _1=\varLambda _2$.

Proof

Firstly, we observe that, with the assumption that $f\in K[x_1,\dots ,x_{s_1}]$, by Theorem 1, $St_1$ generally true is equivalent to $St_3$ generally true; the same happens with $St_2$ and $St_4$. If we prove that $St_3$ is generally true if and only if so is $St_4$, we are done. Indeed, this follows trivially from Lemma 2, since $St_3=St_4$.

In addition, equality (6) of Lemma 2 and the inclusion $\varLambda _1\subseteq \varLambda _2$ tell us that

$$\begin{aligned}&\Big (H^e+\mathcal {H}_1^e+(f\cdot t -1)+(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_{s_1}]\\&\quad \subseteq \Big (H^e+\mathcal {H}_2^e+(f\cdot t -1)+(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_{s_2}]. \end{aligned}$$

The previous inclusion trivially switches to an equality if $\varLambda _1=\varLambda _2$. $\square$

Corollary 3

With the above notation, $St_A$ is generally true if and only if $St_B$ is generally true as well.

Proof

Since $St_A$ and $St_1$ are the same statement, Theorem 2 enables us to state that $St_A$ generally true is equivalent to $St_2$ generally true; i.e., $\big (H^{e}+\mathcal {H}_2^e+(f\cdot t-1)^e +(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_{s_2}]\ne (0)$. Let us prove that

$$\begin{aligned}&\Big (H^e+\mathcal {H}_2^e+(f\cdot t-1) +(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_{s_2}]\nonumber \\&\quad =\texttt {Sat}\Big (\Big (H_2^e+\mathcal {H}_2^e+(T\cdot t'-1)\Big )\cap K[x_1,\dots ,x_{s_2}],f\Big ). \end{aligned}$$

(7)

Indeed, by equality (1), the reasoning in (4) and $f\in K[x_1,\dots ,x_{s_1}]$, we have that

$$\begin{aligned}&\texttt {Sat}\big ((H_2^e+\mathcal {H}_2^e+(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_{s_2}],f) \\&=\texttt {Sat}\big (\texttt {Sat}(H^e,f)+\mathcal {H}_2^e+(T\cdot t'-1),f\big )\cap K[x_1,\dots ,x_{s_2}]\\&=\texttt {Sat}\big (H^e+\mathcal {H}_2^e+(T\cdot t'-1),f\big )\cap K[x_1,\dots ,x_{s_2}]\\&=\big (H^e+\mathcal {H}_2^e+(T\cdot t'-1)+(f\cdot t-1)\big )\cap K[x_1,\dots ,x_n,t']\cap K[x_1,\dots ,x_{s_2}]\\&=\big (H^e+\mathcal {H}_2^e+(f\cdot t-1)+(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_{s_2}]. \end{aligned}$$

Therefore, (7) is proved and then $\big (H^e+\mathcal {H}_2^e+(f\cdot t-1) +(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_{s_2}]\ne (0)$ if and only if $\big (H_2^e+\mathcal {H}_2^e+(T\cdot t'-1)\big )\cap K[x_1,\dots ,x_{s_2}]\ne (0)$; i.e., $St_2$ is generally true if and only if $St_B$ is generally true.

In conclusion, $St_A$ generally true is equivalent to $St_B$ generally true. $\square$

6 Our experiences

In this section, we would like to present a particular example in order to show in some detail the described situation, having the calculations been carried out using the software Singular [9] in the FinisTerrae 2 supercomputer. Our example is based on the already cited theorem about the orthic triangle taken from [8, Example 6 of Section 5]. We wish to show that the orthic triangle associated with an equilateral triangle is also equilateral (see Fig. 1). Since we want to address the theorem from the point of view of discovery, we decide to ignore the hypothesis about the original triangle being equilateral and take a completely arbitrary one, with the purpose of obtaining, automatically, a necessary condition on this general triangle for the corresponding orthic triangle to be equilateral.

So, we take A(0, 0), $B(x_1,0)$ and $C(x_2,x_3)$ as the vertices of the main triangle, and set $D(x_2,0)$, $E(x_4,x_5)$ and $F(x_6,x_7)$ the vertices of the orthic one. The independent variables are $\{x_1,x_2,x_3\}$. We force the segments $\overline{AE}$ and $\overline{BC}$ to be perpendicular, as well as E to be collinear with B and C; analogously, $\overline{BF}$ and $\overline{AC}$ must be perpendicular, and F must be aligned with A and C. By construction, it is obvious that the point D is collinear with A and B, and that $\overline{CD}$ is perpendicular to $\overline{AC}$. As for our desired conclusion, we state it using two polynomials, each one forcing two sides of the orthic triangle to have the same length; i.e., one for $DE = DF$, and another for $DE = EF$. We deal with them separately, distinguishing between theses T and $T'$, respectively, and theorems $H\Longrightarrow T$ and $H\Longrightarrow T'$.

Fig. 1

Orthic triangle

Besides the main hypotheses, we choose to add (based on human intuition and hoping to help to simplify the computations) as non-degeneracy conditions those which force the triangle ABC not to collapse to a line, i.e., $x_1\ne 0$ and $x_3\ne 0$. These two conditions can be summarized in just one: $f=x_1x_3\ne 0$. We introduce this new hypothesis $f\ne 0$, both employing Rabinowitsch’s trick and by saturation, in each of the two theorems $H\Longrightarrow T$ and $H\Longrightarrow T'$. It is easy to check that any of the statements $H_1\Longrightarrow T$, $H_2\Longrightarrow T$, $H_1\Longrightarrow T'$ and $H_2\Longrightarrow T'$ is generally false. However, different formulations of the introduced non-degeneracy hypothesis can lead to different sets of additional affirmative hypotheses for the discovery of a true statement. More precisely, for the theorem $H\Longrightarrow T$, we get (notation as in the previous section):

$$\begin{aligned} \mathcal {H}_2^{T}=x_1\cdot \mathcal {H}_1^{T}=\Big (x_1 \, (x_1-2x_2)\, \Big (x_1x_2-x_2^2+x_3^2\Big ) \, \Big (-x_1x_2+x_2^2+x_3^2\Big )\Big ). \end{aligned}$$

Nevertheless, for the theorem $H\Longrightarrow T'$, we obtain

$$\begin{aligned} \mathcal {H}_1^{T'}=\mathcal {H}_2^{T'}=\Big (x_2 \, \Big (-x_1^2+x_2^2+x_3^2\Big ) \,\Big (-x_1^2x_2+2x_1x_2^2+2x_1x_3^2-x_2^3-x_2x_3^2\Big )\Big ). \end{aligned}$$

We appreciate that the factor $x_1$, which was forced to be different from zero by introducing the non-degeneracy hypothesis, appears—as a zero condition—in $\mathcal {H}_2^{T}$, due to the early closure of the saturation, similarly to what happens in Example 5. Informally speaking, we can say that adding the negation $x_1x_3\ne 0$ is not so conclusive when we deal with saturation as it is when employing Rabinowitsch’s trick.

It is also trivial to check that, if the triangle ABC is equilateral, the additional conditions in $\mathcal {H}_1^{T}$, $\mathcal {H}_2^{T}$, $\mathcal {H}_1^{T'}$ or $\mathcal {H}_2^{T'}$ all vanish. That is, equilateral triangles yield equilateral orthic triangles. Nevertheless, we also see that there are other possible configurations for the given triangle which make these additional, necessary conditions to vanish: configurations that should be carefully analyzed, since, if also sufficient, they would bring some unexpected statements regarding the regularity of the orthic triangle.

Now, a direct computation shows that the statement $St_B$ (according to the previous section notation) is generally true for both T and $T'$, but by brute force we are not able to decide if $St_A$ is, as well, generally true. Yet, applying our precedent results, we can conclude that not only is $St_A=St_1$ generally true, but the same applies to $St_2$ and $St_3=St_4$, too. Moreover, the calculations for $St_4$ reveal that, in addition to being generally true, we do not need to consider non-degeneracy conditions both for T and for $T'$; again, and since $\varLambda _1^{T} =\varLambda _2^{T}=\varLambda _1^{T'}=\varLambda _2^{T'}=\{x_1,x_3\}$, Theorem 2 allows us to state that $St_A=St_1$ and $St_2$ do not need additional non-degeneracy conditions as well.

What is interesting to emphasize here is that the computer is not able to arrive at these conclusions by directly following the Rabinowitsch approach in $St_A$ and confirming that the theses T and $T'$ are generally true, while it encounters no difficulties with the saturation approach of $St_B$ or $St_4$. So, we think that this example clearly illustrates the practical advantages, in some cases, of using saturation instead of Rabinowitsch’s trick. Also, the example highlights the applicability of the results in the previous section.

Yet, we should make clear here that we do not know the reason for the failure of the FinisTerrae 2 supercomputer concerning the computation, via Singular, of the Rabinowitsch approach for this particular example. We like to note that the saturation-based computation uses Singular’s implementation of saturation which does not involve elimination³. We want to thank the referees for pointing out this, as well as for bringing up our attention to reference [4], for a detailed account of the complex, reciprocal relation between saturation and elimination (saturation via elimination, elimination via saturation).

7 Conclusions

At this point, the reader could wonder: which one of the presented methods is better? The answer is not totally objective. We encourage to implement the saturation method in the automated proving and discovery software, due to the scarce effectiveness of Rabinowitsch’s trick when dealing with negative theses and to the practical objections exposed in Sect. 5. But there is a counterpart: by considering the early closure of the saturation $\texttt {Sat}(H,f)$, we can lose essential information about the negation $\lnot \{f=0\}$, and f may appear further as a zero equation in the additional hypotheses yielded by saturation, transgressing, in a certain sense, the restrictions imposed by the introduced non-degeneracy conditions. This fact is precisely what differentiates both methods, and what could persuade us to employ sometimes Rabinowitsch’s trick, if we want to preserve the negation of f until the end of the procedure, in order to remain faithful to some a priori stated non-degeneracy condition. In our opinion, in this case, it should be decided by the user, through the corresponding dialogue with the involved automatic theorem proving software.

Finally, we must recall here the existence of some new algorithmic tools to deal with constructible sets (as detailed in the footnote¹) that deserve future consideration and implementation in some dynamic geometry program provided with automated reasoning modules.