×

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

Summary: 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.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
14Q20 Effectivity, complexity and computational aspects of algebraic geometry

Software:

SINGULAR; GeoGebra
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abánades, M.; Botana, F.; Kovács, Z.; Recio, T.; Sólyom-Gecse, C., Development of automatic reasoning tools in GeoGebra, ACM Commun. Comput. Algebra, 50, 3, 85-88 (2016) · Zbl 1365.68431 · doi:10.1145/3015306.3015309
[2] Abánades, M., Botana, F., Kovács, Z., Recio, T., Sólyom-Gecse, C.: Towards the automatic discovery of theorems in GeoGebra. In: Greuel, G., Koch, T., Paule, P., Sommese, A. (eds.) International Congress on Mathematical Software, pp. 37-42. Springer, New York (2016) · Zbl 1434.68636
[3] Barakat, M., Lange-Hegermann, M.: An algorithmic approach to Chevalley’s theorem on images of rational morphisms between affine varieties (2019). arXiv:1911.10411v2
[4] Barakat, M., Lange-Hegermann, M., Posur, S.: Elimination via saturation (2017). arXiv:1707.00925
[5] Botana, F.; Recio, T., On the unavoidable uncertainty of truth in dynamic geometry proving, Math. Comput. Sci., 10, 1, 5-25 (2016) · Zbl 1357.68197 · doi:10.1007/s11786-016-0246-4
[6] Chou, S.C.: Mechanical geometry theorem proving. Mathematics and its applications, vol. 41. D. Reidel Publishing Co., Dordrecht (1988) (With a foreword by Larry Wos) · Zbl 0661.14037
[7] Cox, D.A., Little, J., O’Shea, D.: Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra. Undergraduate Texts in Mathematics, 4th edn. Springer, Cham (2015) · Zbl 1335.13001
[8] Dalzotto, G.; Recio, T., On protocols for the automated discovery of theorems in elementary geometry, J. Automat. Reason., 43, 2, 203-236 (2009) · Zbl 1184.68458 · doi:10.1007/s10817-009-9133-x
[9] Decker, W., Greuel, G.M., Pfister, G., Schönemann, H.: Singular 4-1-2—A computer algebra system for polynomial computations (2019). http://www.singular.uni-kl.de
[10] Kapur, D., A refutational approach to geometry theorem proving, Artif. Intell., 37, 1-3, 61-93 (1988) · Zbl 0678.68094 · doi:10.1016/0004-3702(88)90050-1
[11] Kapur, D., Sun, Y., Wang, D., Zhou, J.: The generalized Rabinowitsch trick. In: Applications of computer algebra, Springer Proc. Math. Stat., vol. 198, pp. 219-229. Springer, Cham (2017) · Zbl 1396.13025
[12] Mishra, B., Algorithmic Algebra. Texts and Monographs in Computer Science (1993), New York: Springer, New York · Zbl 0804.13009
[13] Montes, A.; Recio, T., Generalizing the Steiner-Lehmus theorem using the Gröbner cover, Math. Comput. Simul., 104, 67-81 (2014) · Zbl 1467.68231 · doi:10.1016/j.matcom.2013.06.006
[14] Rabinowitsch, JL, Zum Hilbertschen Nullstellensatz, Math. Ann., 102, 1, 520 (1930) · JFM 55.0103.04 · doi:10.1007/BF01782361
[15] Recio, T.; Vélez, MP, Automatic discovery of theorems in elementary geometry, J. Automat. Reason., 23, 1, 63-82 (1999) · Zbl 0941.03010 · doi:10.1023/A:1006135322108
[16] Recio, T., Vélez, M.P.: An introduction to automated discovery in geometry through symbolic computation. In: Numerical and symbolic scientific computing, Texts Monogr. Symbol. Comput., pp. 257-271. Springer, New York (2012) · Zbl 1250.65040
[17] Wu, WT, On the decision problem and the mechanization of theorem-proving in elementary geometry, Sci. Sinica, 21, 2, 159-172 (1978) · Zbl 0376.68057
[18] Zhou, J.; Wang, D.; Sun, Y., Automated reducible geometric theorem proving and discovery by Gröbner basis method, J. Automat. Reason., 59, 3, 331-344 (2017) · Zbl 1425.68383 · doi:10.1007/s10817-016-9395-z
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.