# 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{}‎ ‎$ , ‎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.‎