Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch
- PDF / 369,609 Bytes
- 16 Pages / 439.37 x 666.142 pts Page_size
- 109 Downloads / 178 Views
Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch’s trick Manuel Ladra1
· Pilar Páez-Guillán2 · Tomás Recio3
Received: 26 May 2019 / Accepted: 12 May 2020 © The Royal Academy of Sciences, Madrid 2020
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. Keywords Automated proving · Automated discovery · Non-degeneracy conditions · Rabinowitsch’s trick · Saturation Mathematics Subject Classification 68T15 · 14Q99 · 03B35 · 51-04
B
Manuel Ladra [email protected] Pilar Páez-Guillán [email protected] Tomás Recio [email protected]
1
Departamento de Matemáticas, Instituto de Matemáticas, Universidad de Santiago, Santiago de Compostela, Spain
2
Departamento de Matemáticas, Instituto de Matemáticas, Universidad de Santiago, Santiago de Compostela, Spain
3
Departamento de Matemáticas, Estadística y Computación, Universidad de Cantabria, Santander, Spain 0123456789().: V,-vol
123
162
Page 2 of 16
M. Ladra et al.
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-degen
Data Loading...
