Wu’s Method

By | September 13, 2020

Here is the summary of last section; section 5 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 want to introduce an algorithmic method for proving theorems in Euclidean geometry based on systems of polynomial equations. ‎This ‎method ‎is ‎more ‎commonly ‎used ‎than‎ Gröbner basis method in practice because it is usually more efficient. However both of these methods make essential use of a division algorithm to determine whether a polynomial is in a given ideal or not.‎


‎Let‎ f,g ‎be ‎two ‎polynomials ‎in ‎the ‎ring‎ k[x_1, \ldots, x_n, y] ‎and ‎written ‎in ‎the ‎form:‎

 ‎‎‎‎f =‎ ‎c_p ‎y^p +‎ ‎\ldots ‎+c_1 y‎ ‎+c_0,\\‎ g =‎ ‎d_m ‎y^m +‎ ‎\ldots +‎ ‎d_1 y‎ +‎ ‎d_0.‎ 

‎Proposition 1. ‎Let‎ f,g \in k[x_1, \ldots, x_n, y] be as above, and assum ‎ m \le p ‎and‎ ‎ d_m \neq 0 .‎‎

‎(i) ‎There ‎is ‎an ‎equation‎ ‎

 {d_m}^s f = qg + r  

Where q,r \in k[x_1, \ldots, x_n, y] ‎, s \ge 0 , ‎and ‎either‎ ‎ r = 0 ‎or ‎the ‎degree ‎of‎ r ‎in‎ ‎ y ‎is ‎less ‎than‎ m .‎

‎‎(ii) r \in <f,g> ‎in ‎the ‎ring‎ ‎ k[x_1, \ldots, x_n, y] .‎

‎‎We ‎use ‎the ‎notation‎ ‎ deg(h,y) ‎for ‎the ‎degree ‎of ‎the ‎polynomoal‎ h ‎in ‎the ‎variable‎ y ‎and‎ ‎ LC(h,y) ‎for ‎leading ‎coefficient ‎of‎ h ‎as a‎ ‎polynomial ‎in ‎y, ‎the ‎coefficient ‎of‎ y^{deg(h,y)} ‎in‎ h .‎

Pseudodivision algorithm with respect to ‎ y

‎‎ ‎Input: ‎f, \ g‎ ‎\\‎ ‎Output: q, \ r \\‎ ‎\\ m ‎:= ‎deg(g,y); \hspace{0.3cm} ‎d:= ‎LC(g,y)\\‎ r ‎:= ‎f; \hspace{0.3cm} ‎q:= 0‎ ‎\\‎ WHILE \hspace{0.3cm} r‎ ‎\neq 0 \hspace{0.3cm} ‎‎ ‎AND \ ‎deg(r,y) ‎\ge m‎ \hspace{0.3cm} ‎DO\\‎ ‎\hspace{1cm} ‎r:= ‎dr -‎ ‎LC(r,y) g y^{deg(r,y) - m}\\‎ ‎\hspace{1cm} ‎q:= ‎dq + ‎LC(r,y) ‎y^{deg(r,y) - m}‎\\‎ RETURN \hspace{0.3cm} q, \ r‎‎‎‎‎ ‎ ‎‏‎

[WHILE loop will be executed at most ‎ p-m+1 times, and so for ‎ s in d^s f = qg + r we have ‎ s \le p-m+1 .‎]‎‎‎

The ‎polynomial‎ q ‎is ‎called‎ ‎pseudoquotient ‎and ‎the ‎polynomial‎ r ‎is ‎called‎ ‎ pseudoremainder ‎of‎ ‎ f ‎on ‎pseudodivision ‎by‎ ‎ g ‎with ‎respect ‎to ‎the ‎variable‎ y . ‎For‎ pseudoremainder we use the notation Rem(f,g,y) .‎

In Maple

‎‎‎In Maple, ‎to obtain the Rem(f,g,y) we can use the function prem ‎that‎ returns the pseudo-remainder ‎ r ;‎

  r :=prem(f,g,y)  

Now ‎by ‎what ‎has been ‎said ‎about ‎hypotheses, ‎variables ‎and ‎assuming‎ ‎ V^{‎\prime‎} ‎ ‎irreducible, ‎we ‎want ‎to ‎prov‎e that ‎ g \in ‎\textbf{I} (V^{\prime}) .‎ ‎‎

For ‎this ‎we ‎have 2‎ ‎step; ‎first ‎using ‎pseudodivision ‎to ‎reduce ‎the ‎hypotheses ‎to a ‎‎system ‎of ‎polynomials‎ ‎ f_j ‎that ‎are ‎in‎ ‎triangular form ‎in ‎the ‎variables‎ ‎ x_1, \ldots , x_n , ‎and ‎second, ‎usin‎g successive ‎pseudodivision ‎of ‎the ‎conclusion‎ g ‎with ‎respect ‎to ‎each ‎of ‎the ‎variables‎ x_j ‎to ‎determine ‎whether‎ g ‎vanishes ‎on‎ V^{\prime} .‎

Step 1. Reduction to Triangular Form

1. ‎Among ‎the ‎hypotheses ‎(‎ h_j ‎), ‎find ‎all ‎polynomials ‎containing ‎th‎e variable x_n . Call the set of such polynomials S .‎

‎‎2. ‎If‎ ‎‎ |S| = 1 ‎, then we can rename the polynomials, making that polynomial ‎ {f^{‎\prime‎}}_n , ‎and ‎our ‎system ‎of ‎polynomials ‎will ‎have ‎the ‎form:‎

  ‎{f^{\prime}}_1 = {f^{\prime}}_1 (u_1, \ldots ,u_m, x_1, \ldots , x_{n_1})\\‎ ‎‎\hspace{2cm} ‎‎\vdots‎\\  ‎‎‎‎\hspace{6cm} ‎*‎ \\ ‎{ ‎‎f^{\prime}}_{n-1} = {f^{\prime}}_{n-1} (u_1, \ldots ,u_m, x_1, \ldots , x_{n_1})\\ { f^{\prime}}_{n} = {f^{\prime}}_{n} (u_1, \ldots ,u_m, x_1, \ldots , x_n)\\  

3. ‎If‎ |S| > 1 , but some element of ‎ S ‎has ‎degree‎ ‎1 ‎in ‎‎ x_n , ‎then ‎we ‎can ‎take‎ { f^{\prime}}_{n} ‎as ‎that ‎polynomial ‎and ‎replace ‎all ‎other ‎hypotheses ‎in‎ ‎ S ‎by ‎their‎ Rem(all \ other \ hypothses, { f^{\prime}}_{n} , x_n ) . ‎Again ‎we ‎obtain a‎ ‎system ‎like‎ ‎ * .‎‎‎

4. ‎If‎ |S| > 1 , but none has degree 1 ‎in‎ ‎ x_n , ‎then ‎pick‎ a, b \in S ‎where‎ 0 ‎< ‎deg(b, x_n) \le deg (a, x_n) ‎ ‎and ‎compute ‎the‎ r = Rem(a,b,x_n) . ‎Then:‎‎‎

4.1. ‎If‎ deg(r, x_n) \ge 1 ‎, then replace ‎ S ‎by‎ (S \setminus \{a\} ) \cup \{r\} ‎and ‎repeat ‎either 4 ‎‎(if deg(r,x_n) \ge 2 ‎) ‎or 3‎ ‎(if ‎ deg(r,x_n) = 1 ‎).‎‎‎

4.2. ‎If‎ deg(r, x_n) = 0 then replace ‎ S ‎by‎ S \setminus \{a\} ‎and ‎repeat ‎either 4‎ ‎(if the new ‎ S has \ge 2 elements‎)‎ ‎or 2‎ ‎(if the new S has only one element‎).‎‎

‎Eventually ‎we ‎are ‎reduced ‎to a‎ ‎system ‎of ‎polynomials ‎of ‎the ‎form‎ ‎ * ‎again.‎

‎‎‎Proposition 2. ‎Suppose ‎that‎ f_1 = \ldots = f_n = 0 ‎are ‎the ‎triangular ‎equations ‎obtained ‎from‎ ‎ h_1 = \ldots = h_n = 0 ‎by ‎the ‎above ‎reduction ‎algorithm. ‎Then‎

  V^{\prime} \subseteq V = ‎\textbf{V}(h_1, \ldots , h_n) ‎\subseteq‎ ‎\textbf{V}(f_1, \ldots , f_n)‎        ‎‎

Since‎ ‎ <f_1 , \ldots , f_n> \subseteq <h_1 , \ldots , h_n> ‎then V = \textbf{V}(h_1, \ldots , h_n) \subseteq \textbf{V}(f_1, \ldots , f_n) …‎

Step 2. Successive Pseudodivision

Now we compute‎

  ‎R_{n-1} = Rem (g,f_n,x_n),\\ ‎R_{n-2} = Rem (R_{n-1},f_{n-1},x_{n-1}),\\‎ ‎‎ ‎‎‎\vdots ‎\\  ‎‎‎‎\hspace{4cm} ‎**‎ \\ ‎R_1 =‎ ‎Rem(R_2,f_2,x_2),\\‎ R_0 = ‎Rem(R_1,f_1,x_1).‎ ‎‎‎‎‎

Theorem 3. ‎Consider ‎the ‎set ‎of ‎hypotheses ‎and ‎conclusion ‎for a ‎‎geometric ‎theorem. ‎Let‎ ‎ R_0 ‎be ‎the ‎final ‎remainder ‎computed ‎by ‎the ‎successive ‎pseudo‎division of ‎ g ‎as ‎in ‎‎ ** , ‎using ‎the ‎system ‎of ‎polynomial‎s f_1, \ldots , f_n ‎in ‎triangular ‎form‎ * . ‎Let‎ d_j ‎be ‎the ‎leading ‎coefficient ‎of‎ ‎ f_j ‎as a‎ ‎polynomial ‎in‎ x_j ‎(so d_j is a polynomial in u_1, \ldots, u_m ‎and x_1, \ldots , x_n ‎‎). ‎Then:‎‎‎

(i) ‎There ‎are ‎nonnegative ‎integers‎ ‎ s_1, \ldots, s_n ‎and ‎polynomoals‎ ‎ A_1, \ldots , A_n ‎in ‎the ‎ring‎ ‎ ‎\mathbb{R}[u_1,\ldots,u_m,x_1,\ldots,x_n] ‎such ‎that‎

 {d^{s_1}}_1 \ldots {d^{s_n}}_n g = A_1 f_1 + \ldots + A_n f_n + R_0  

(ii) ‎If‎ R_0 ‎is ‎the ‎zero ‎polynomial, ‎then‎ g ‎is ‎zero ‎at ‎every ‎point ‎of‎ ‎‎

 V^{\prime} \setminus ‎\textbf{V}(d_1 d_2 \ldots d_n) \ \subseteq ‎\mathbb{R}^{m+n}‎‎  .‎‎‎

We ‎can ‎easily ‎trying ‎the‎ ‎Circle Theorem of Apollonius ‎by ‎Wu’s ‎method ‎and ‎investigate ‎these ‎two ‎steps‎.

For ‎tools ‎and ‎package ‎we ‎can ‎refere ‎to ‎the ‎chapeter‎ ‎“An implementation of the characteristic set method in Maple”} ‎of ‎the ‎book‎ ‎”Automated Practical Reasoning“‎.

Leave a Reply

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