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

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.