Automatic Geometric Theorem Proving

By | September 13, 2020

Here is the summary of section 4 of Chapter 6; Robotics and Automatic Geometric Theorem Proving of the book {Ideals, Varieties, and Algorithms} By‎ David A. Cox , John Little and Donal O’Shea

Here we intend to introduce this idea that the hypotheses and conclusions of a large class of geometric theorems can be expressed as ‎\textit{polynomial equations} ‎between ‎the ‎coordinate‎s of collections of points specified in the statements.‎

When a theorem describes the constructing the geometric configuration, some of the coordinates of some points wil be ‎arbitrary, ‎whereas ‎the ‎remaining ‎coordinates ‎of ‎points ‎will‎ ‎determined (possibly up to a finite number of choices) ‎by ‎the ‎arbitrary ‎ones.‎

We use variables ‎u_i ‎ ‎to ‎indicating ‎arbitrary ‎coordinates, also ‎we ‎use‎ ‎ x_j ‎ ‎‎to ‎denote ‎the ‎other ‎coordinates‎ ‎that ‎determine ‎by‎ ‎ u_i ‎ ‎.‎‎

We can understand better what is said above, by the following example:‎

The Circle Theorem of Apollonius. ‎Let ‎‎ ‎ ABC ‎ ‎be a‎ ‎right ‎triangle ‎in ‎the ‎plane, ‎with ‎right ‎angle ‎at‎ ‎ A ‎ . ‎The ‎midpoints ‎of ‎the ‎three ‎sides ‎and ‎the ‎foot ‎of ‎the ‎altitude ‎drawn ‎from‎ ‎ A ‎ ‎to‎ ‎ ‎ ‎\bar{BC}‎ ‎ ‎all ‎lie ‎on ‎one ‎circle.‎‎

‎We consider ‎ ‎ A=(0,0) ‎ ,‎ ‎ B=(u_1,0) ‎ ‎and‎ ‎ C=(0,u_2) ‎ . ‎Now ‎we ‎constructing ‎three ‎midpoint‎s of the sides, with coordinates ‎‎ ‎ M_1 = (x_1,0)‎ ‎ ,‎ ‎ ‎ M_2 = (0,2) ‎ , ‎and‎ ‎ M_3 = (x_3,x_4) ‎ . ‎Easily ‎we ‎obtain ‎the ‎hypotheses in the form of equations as below:‎

‎ ‎ h_1 =‎ ‎2x_1 -‎ ‎u_1 ‎=0,\\ h_2 ‎=2x_2 - ‎‎u_2 =‎ ‎0,\\‎ h_3 =‎ ‎2x_3 - ‎u_1 =‎ ‎0,\\‎ h_4 =‎ ‎2x_‎4 -‎ ‎u_2 =‎ ‎0‎.\\‎ ‎ 

Also we denote the foot of the altitude drawn from ‎ A ‎ to ‎ \bar{BC} ‎ by ‎ H = (x_5,x_6) ‎ , ‎and ‎we ‎obtain ‎two ‎more ‎hypothe‎ses:‎

‎ ‎ ‎h_5 = u_2 x_5 + u_1 x_6 - u_1 u_2 = 0,\\‎ h_6 =‎ ‎u_1 ‎x_5 -‎ ‎u_2 ‎x_6 =‎ ‎0.‎\\ ‎

To proving the theorem, we construct the circle containing the noncollinear triple ‎ M_1,M_2,M_3 ‎ , ‎then‎ ‎ H ‎ ‎must ‎lie ‎on ‎this ‎circle‎.‎

‎We ‎call ‎the ‎center ‎of ‎this ‎circle‎ ‎ O=(x_7,x_8) ‎ ‎and ‎derive ‎two ‎additional ‎hypotheses:‎‎‎

 ‎M_1 O‎ =‎ ‎M_2 O‎ :‎ ‎h_7 =‎ ‎(x_1 - x_7)^2 +‎ ‎{x_8}^2 - ‎‎‎{x_7}^2 -‎ ‎(x_8 - x_2)^2 =‎ ‎0,\\‎ ‎M_1 O = M_3 O : h_8 = (x_1 - x_7)^2 + (0-x_8)^2 - (x_3 - x_7)^2 - (x_4 - x_8)^2 = 0.\\ ‎‎

And then the conclusion is ‎ ‎ HO = M_1 O ‎ , ‎which ‎takes ‎the ‎form:‎

‎ ‎ g = (x_5 - x‎_7)^2 + (x_6 - x_8)^2 - (x_1 - x_7)^2 - {x_8}^2 = 0 ‎

In ‎general ‎we ‎have ‎hypotheses ‎as:‎‎

 ‎‎h_1(u_1, \ldots ,u_m,x_1, \ldots, x_n) = 0,\\‎‎‎‎ ‎  \vdots‎ * ‎ ‎h_n(u_1, \ldots ,u_m,x_1, \ldots, x_n) = 0.  

‎And the conclusion as:‎

 g(u_1, \ldots ,u_m,x_1, \ldots, x_n) = 0 ‎‎‎ ‎ 

‎Now the question ‎is‎:‎‎

How ‎can ‎we ‎deduce algebraically ‎the ‎fact ‎that‎ ‎ ‎ g ‎ ‎follows ‎from‎ ‎ ‎ h_1, \ldots ,h_n ‎ ‎?‎‎‎

The ‎basic ‎idea ‎is ‎that ‎we ‎want‎ ‎ ‎ g ‎ ‎vanish ‎whenever‎ ‎ h_1, \ldots ,h_n ‎ do. We observe that the hypotheses * are equations that define a variety‎

‎ ‎ V = ‎\textbf{V}(h_1, \ldots ,h_n) \subseteq ‎\mathbb{R}^{m+n}‎‎ ‎ 

Definition 1. ‎The ‎conclusion‎ ‎ ‎ g ‎ ‎ ‎\textbf{follows strictly} ‎from ‎the ‎hypotheses‎ ‎ h_1, \ldots ,h_n ‎ if ‎ ‎ g \in ‎\textbf{I}(V) \subseteq ‎\mathbb{R}[u_1, \ldots, u_m,x_1, \dots, x_n]‎‎ ‎ , ‎where‎ ‎ ‎V = \textbf{V}(h_1, \ldots ,h_n)‎ ‎ ‎‏.‎‎

Proposition 2. ‎If‎ ‎ ‎ g \in ‎\sqrt{<h_1, \ldots, h_n>}‎ ‎ , ‎then‎ ‎ g ‎ ‎follows ‎strictly ‎from‎ ‎ ‎ h_1, \ldots, h_n ‎ ‎.‎‎

Definition 3. ‎Let‎ ‎ W ‎ ‎be ‎an ‎irreducible ‎variety ‎in ‎the ‎affine ‎space‎ ‎ ‎\mathbb{R}^{m+n}‎ ‎ ‎with ‎coordinate‎s ‎ ‎ u_1,\ldots,u_m,x_1,\ldots,x_n ‎ . ‎We ‎say ‎that ‎the ‎functions‎ ‎ u_1,\ldots,u_m ‎ ‎are‎ ‎\textbf{algebraically independent on} ‎‎ ‎ W ‎ ‎if ‎no ‎nonzero ‎polynomial ‎in ‎the‎ ‎ ‎ u_i ‎ ‎alone ‎vanishes ‎identically ‎on‎ ‎ W ‎ .‎‎‎

Equivalently,‎ ‎ u_1,\ldots,u_m ‎ are algebraically independent on ‎ W ‎ ‎if‎‎

 \textbf{I}(W) \cap \mathbb{R}[u_1, \ldots, u_m] = \{0\} ‎ .

‎From ‎theorem 2‎ ‎of ‎chapter 4‎ ‎we ‎know ‎that ‎if‎ ‎ ‎ V ‎ ‎is an ‎affine ‎variety‎, then ‎ ‎ V ‎ ‎can ‎be ‎written ‎as a‎ ‎finite ‎union‎

‎ ‎ V = W_1 \cup \ldots \cup W_p \cup U_1 \cup \ldots \cup U_q ‎ 

Where the components are irreducible and ‎ u_1, \ldots , u_m ‎ ‎are ‎algebraically ‎independent ‎on ‎the ‎components‎ ‎ W_i ‎ ‎and ‎are ‎not‎ algebraically independent on the components ‎ U_j ‎ ‎. ‎‎ ‎

\bigg ( V‎^{\prime} =‎ ‎W_1 ‎\cup ‎\ldots ‎\cup ‎W_p ‎\subseteq ‎V‎ \bigg ) ‎ ‎‎

Definition 4. ‎The ‎conclusion‎ ‎ ‎ g ‎ ‎‎follows generically ‎from ‎the ‎hypotheses‎ ‎ ‎ h_1, \ldots, h_n ‎ ‎if‎ ‎ g \in ‎\textbf{I}( ‎V^{\prime}) \subseteq \mathbb{R}[u_1, \ldots, u_m,x_1, \dots, x_n] ‎ ‎ , ‎where, ‎as ‎above,‎ ‎ ‎ V^{\prime} ‎\subseteq ‎\mathbb{R}^{m+n}‎ ‎ ‎ ‎is ‎the ‎union ‎of ‎the ‎components ‎of ‎the ‎variety‎ ‎ V = ‎\textbf{V}(h_1, \ldots , h_n)‎ ‎ ‎on ‎which ‎the‎ ‎ u_i ‎ ‎are ‎agebraically ‎independent.‎

‎[A geometric theorem is true ‎ ‎ ‎\longleftrightarrow‎ ‎ ‎Conclusion(s) follow generically from its hypotheses.‎‎]

Now ‎the question ‎is:‎‎‎

Can ‎we ‎determine ‎when‎ ‎ g \in \textbf{I}( V^{\prime}) ‎ ‎‏?‎‎‎

‎Proposition 5. ‎In ‎the ‎above ‎situation ,‎ ‎‎ ‎ g ‎ ‎follows ‎generically ‎from‎ ‎ ‎ h_1, \ldots, h_n ‎ ‎whenever ‎there ‎is ‎some ‎nonzero ‎polynomial‎ ‎ ‎ c(u_1, \ldots, u_m) \in ‎\mathbb{R}[u_1, \ldots, u_m]‎ ‎ ‎such ‎that‎

‎ ‎ c . g \in ‎\sqrt{H} ‎

Where ‎ ‎ H ‎ ‎is ‎the ‎ideal ‎generated ‎by ‎the ‎hypotheses‎ ‎ ‎ h_i ‎ ‎in‎ ‎ ‎\mathbb{R}[u_1, \ldots, u_m,x_1, \dots, x_n] ‎ .‎

This ‎proposition ‎helps ‎us ‎to ‎determine ‎whether‎ ‎ g \in \textbf{I}( V^{\prime}) ‎ or not, in other words, it gives us a criteria for evaluation that the geometric theorem is true or not‏.‎‎

‎Also ‎its ‎advantage ‎is that it ‎doesn’t ‎need ‎the ‎decomposition ‎of‎ ‎ ‎ V ‎ ‎into ‎its ‎irreducible ‎components.‎

Leave a Reply

Your email address will not be published. Required fields are marked *