# 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.‎

## Pseudodivision

‎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 $ ‎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‎ ‎ $ \subseteq $ ‎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“‎.