%Keywords: Geometry theorem proving, algorithmic commutative algebra,
%radical decomposition

\documentstyle [11pt]{article}
\title{Radical decomposition and geometry theorem proving}
\author{Michael Kalkbrener\\Department of Mathematics\\
Swiss Federal Institute of 
Technology\\
CH-8092 Zurich, Switzerland}

\textheight     600pt
\textwidth      420pt
\topmargin       18pt
\oddsidemargin   30pt
\evensidemargin  30pt

\date{} 
\newtheorem{theorem}{Theorem}
\newtheorem{example}{Example}
\newtheorem{lemma}{Lemma}



\begin{document}
\maketitle

\section{Introduction}
In the late 70's and early 80's the work of Wu Wen-tsun \cite{Wu78},
\cite{Wu84} has renewed the interest in algebraic approaches to
automated geometry theorem
proving. In the following years it was demonstrated in a number of papers
(see, for instance, \cite{Chou88}, \cite{ChGa90a}, \cite{KoHu85}, 
\cite{KaWa90}, \cite{Wang92a}, \cite{ChSc86}, \cite{Kapu86a}, 
\cite{KuSt86b}) 
that the characteristic set method of Ritt and Wu
as well as the Gr\"obner bases 
algorithm are
useful tools for proving theorems in Euclidean geometry
although the applicability
of the algebraic approach based on these methods 
is limited by the following two restrictions:

\smallskip
\noindent
(a) Geometrical statements cannot be decided in real space but only
in complex space. Therefore theorems in real geometry can only be confirmed 
by proving them in complex space but they cannot be disproved.

\noindent
(b) This approach only works for those geometrical statements whose 
hypotheses and conclusions can be translated into 
algebraic 
equations. 

\smallskip
The reason for the first restriction is that methods like Gr\"obner bases or 
characteristic sets
can decide
the solvability of a system of algebraic equations over algebraically
closed fields only. Fortunately it has turned out that only very few
geometrical statements hold over the reals but not over the complex.
See MacLane $8_3$ in \cite{Kutz88} for an example. Because of
the second restriction we can use this algebraic approach to
prove theorems about 
incidence, parallelism, perpendicularity,
cocircularity, congruence, etc., but not about ``betweenness'', because 
no order predicate is available.

Often a geometrical statement is true only in a ``generic'' sense, i.e.
after certain degenerate situations have been ruled out. Such degenerate
situations typically occur when triangles collapse to a line segment,
circles to a point, etc. and they are usually not explicitly mentioned.
An automatic procedure for proving geometrical statements has to be able to
deal with the problem of such ``degeneracy'' conditions, that means it has
to be able to automatically find suitable nondegeneracy conditions which
make the statement a theorem, if such conditions exist at all.

Hence this algebraic approach to automated geometry theorem
proving leads to the following algebraic problem.
Let $K$ be
a field and $\bar K$ an algebraically
closed field which has infinite transcendence degree over  $K$.
Let $h_1,\ldots,h_m$ and $c$ be polynomials
in $K[x_1,\ldots,x_n]$ 
obtained by 
translating the hypotheses and conclusion of a geometrical statement
into algebraic equations. 
During this translation process a set $X\subset
\{x_1,\ldots,x_n\}$ of independent variables can be identified. 
We assume 
without loss of generality that 
$X=\{x_1,\ldots,x_t\}$.
Now the problem is to decide whether 
\begin{equation}
(\exists d\in K[x_1,\ldots,x_t]\setminus\{0\})(\forall a\in {\bar K}^n) ~
[h_1(a)=\ldots =h_m(a)=0\,\wedge\, d(a)\not= 0 ~\Rightarrow ~c(a)=0], 
\label{f1}
\end{equation}
and, if so, to find such a nondegeneracy condition $d$.

\medskip
For a subset $F$ of $K[x_1,\ldots,x_n]$ the ideal generated by $F$ is denoted
by $\langle F\rangle$, the 
radical of $\langle F\rangle$ by $\sqrt{F}$ 
and the variety of $F$ in ${\bar K}^n$ by
$V(F)$, i.e.
\[ V(F)=\{a\in {\bar K}^n\mid f(a)=0 \hbox{ for every } f\in F\}. \]
Let $V(\{h_1,\ldots,h_r\})=V_1\cup\ldots\cup V_k$ be a decomposition 
into irreducible varieties. We may assume that 
$c$ vanishes on $V_i$ for $i\in\{1,\ldots,l\}$ but not on
$V_j$ for $j\in\{l+1,\ldots,k\}$
for some $l\in\{0,\ldots,k\}$. Define $V':=\bigcup_{i=1}^l V_i$ and 
$V'':=\bigcup_{j=l+1}^k V_j$. Obviously, (\ref{f1}) is true if and only if 
\begin{equation}
\hbox{there exists a non-zero $d\in K[x_1,\ldots,x_t]$ which vanishes on 
$V''$.} \label{103:1}
\end{equation}
In this case $d$ is a nondegeneracy condition. Hence 
the correctness of (\ref{f1}) can be decided by decomposing $V$ into
$V'\cup V''$ and by deciding (\ref{103:1}). 
Both can be done by means of Gr\"obner bases 
and therefore this method is useful for geometry theorem proving
(\cite{Kapu86a}, \cite{ChSc86}):
since $V''=V(I)$, where $I$ is the ideal 
$\langle h_1,\ldots,h_m,cy-1\rangle\cap K[x_1,\ldots,x_n]$
and $y$ is a new variable, we only 
have to check whether $G\cap K[x_1,\ldots,x_t]=\emptyset$, where $G$ is
a Gr\"obner basis of $\langle h_1,\ldots,h_m,cy-1\rangle$ with
respect to a suitable elimination order. 
Instead of Gr\"obner bases the prime decomposition algorithm of Ritt and Wu
can be used (\cite{Ritt50}, \cite{Wu84}).
Based on elimination by pseudodivision and factorization this algorithm
computes for every $i\in\{1,\ldots,k\}$ a so-called irreducible ascending
set $A_i$ which uniquely determines the irreducible variety $V_i$.
For a given $A_i$ we can easily check whether  
$c$ vanishes on $V_i$ and whether there exists a non-zero 
$d_i\in K[x_1,\ldots,x_t]$ which vanishes on $V_i$. Hence
(\ref{103:1}) can be decided.

Therefore computing decompositions of varieties or, equivalently, of radicals
is of great importance in this algebraic approach to
geometry theorem proving.
In this paper
we will
study the decomposition problem in a very general context.
Let $R$ be a
Noetherian commutative ring with identity. 
A system of representations $(S,Rep,{\bf decompose}_R,{\bf split}_R)$ in $R$
consists of

\smallskip
\noindent
(1) a set $S$ of finite subsets of $R$, 

\noindent
(2) a function $Rep$
from $S$ to the set of radicals in $R$ which are unequal to $R$, 

\noindent
(3) an algorithm ${\bf decompose}_R$
that computes for a finite non-empty subset $F$ of $R$ a subset
$\{C_1,\ldots,C_r\}$ of $S$ such that
\[ \sqrt{F}=
\bigcap_{i=1}^r Rep(C_i), \]

\noindent
(4) an algorithm ${\bf split}_R$
that computes for a given $A\in S$ and $f\in R$ 
a pair $(\{B_1,\ldots,B_r\},$ 
$\{C_1,\ldots,C_s\})$ of subsets of $S$ such that
\[
\bigcup_{i=1}^r ap(B_i)=
\{P\in ap(A)\mid f\in P\} \hbox{ and }
\bigcup_{i=1}^s ap(C_i)=
\{P\in ap(A)\mid f\notin P\},
\]
where $ap(C)$ denotes the set of associated prime ideals of $Rep(C)$
for $C\in S$.

\smallskip
Recall that a prime ideal $P\not= R$ is said to have 
height $h$ if there exists at least one chain 
$P_0\subset P_1\subset\ldots\subset
P_h=P$, where the $P_i$ are prime ideals, and there exists no such chain with
more than $h+1$ ideals. We call an ideal unmixed if all its associated
prime ideals have the same height and we 
call $(S,Rep,{\bf decompose}_R,{\bf split}_R)$ a system of 
unmixed resp. prime representations
if $Rep(A)$
is unmixed resp. prime for every $A\in S$.


\medskip
\begin{example}{\rm 
Let $R$ be the multivariate polynomial ring 
$K[x_1,\ldots,x_n]$ over a field $K$. The usual concepts for representing
radicals can be considered as specific systems of representations:
let $S$ be the set of all finite subsets of $R$ which do not generate
$R$. Define
the function $Rep$ 
by $Rep(C):=\sqrt{C}$ for every $C\in S$.
In this case ${\bf decompose}_R$ is the trivial algorithm whose
output is equal to its input. As explained above
the algorithm ${\bf split}_R$ is based on computing localizations by
means of Gr\"obner bases.

Of course we could also define $S$ as the set of finite bases of radicals
unequal to $R$.
In this case the function $Rep$ and the algorithm ${\bf split}_R$ are
defined as above but ${\bf decompose}_R$ is now an algorithm which computes 
for a finite non-empty subset $F$ of $K[x_1,\ldots,x_n]$ a finite basis
of $\sqrt{F}$ (see \cite{GTZ88}, for such an algorithm).

Let $S'$ be the
set of irreducible ascending sets in $K[x_1,\ldots,x_n]$
(see \cite{Wu84}) and $S:=S'\cup\{\{0\}\}$. We define the 
function $Rep$ by mapping $\{0\}$ to the prime ideal $\{0\}$
and every irreducible ascending set $C$ to the prime ideal whose
generic point is given
by $C$. The algorithm ${\bf decompose}_R$ is now the prime decomposition
algorithm of Ritt \cite{Ritt50}. We can decide 
for every $f\in K[x_1,\ldots,x_n]$ and every prime ideal
$P\subset K[x_1,\ldots,x_n]$ given by an irreducible ascending set
whether $f\in P$ using pseudodivision \cite{Wu84}. Since $Rep(A)$ is
prime for
every $A\in S$ we obtain an algorithm ${\bf split}_R$. Therefore
the set of irreducible ascending sets together with the function $Rep$
and these two algorithms is a system of prime representations.
}
\end{example}

\medskip
Our main result is the following theorem.

\medskip
\begin{theorem} If there exists a  
system of (unmixed) representations in $R$ then there exists a  
system of (unmixed) representations in $R[x_1,\ldots,x_n]$.
\end{theorem}

For a similar result on systems of prime representations we refer to
\cite{Kalk93b}.


In section 2 we give a constructive proof of Theorem 1.
In particular, we obtain systems of unmixed representations in 
multivariate polynomial rings over fields.
The basic operation in the algorithms ${\bf decompose}_{R[x_1,\ldots,x_n]}$
and ${\bf split}_{R[x_1,\ldots,x_n]}$ is the 
computation of greatest common divisors of univariate polynomials over 
extension fields. 
No factorization or Gr\"obner bases computation is
needed. 

In section 3 we apply these algorithms to geometry theorem proving. We show
that our approach cannot only be used for deciding
statements of the form (\ref{f1}) but
also for constructing 
simplest nondegeneracy conditions with respect
to lexicographical degree orderings.

\section{Proof of Theorem 1}

Throughout this section let $(S,Rep,{\bf decompose}_R,{\bf split}_R)$ be 
a system of representations in $R$. 
For proving Theorem 1 it suffices to construct
a system of representations $(\bar{S},\overline{Rep},
{\bf decompose}_{R[x]},{\bf split}_{R[x]})$ in the univariate polynomial
ring $R[x]$.
 
\medskip
Let $J$ be an ideal in $R$, $f$ a polynomial in $R[x]$ and $I$ an ideal
in $R[x]$.
The image of $f$ in
$(R/J)[x]$ is denoted by $f^J$, the ideal $\{f^J\mid f\in I\}$ in
$(R/J)[x]$ by $I^J$
and the leading coefficient of $f$ by $lc(f)$. If $J$ is prime the
quotient field of the residue class ring $R/J$ is denoted by $K(J)$.
Let $g\in R[x]$ with $g\not= 0$. There exist
polynomials $pquo(f,g)$ and $prem(f,g)$, called the 
pseudoquotient and pseudoremainder of $f$ and $g$, such that 
\[
(lc(g))^d\cdot f=pquo(f,g)\cdot g + prem(f,g), \]
\[ deg(pquo(f,g))<d
~~~\hbox{ and }~~~deg(prem(f,g))<deg(g), \]
where 
$d:=max(\{ deg(f)-deg(g)+1,0\})$ and $deg(0):=-1$. Note that the 
pseudoquotient and pseudoremainder of $f$ and $g$ are usually not uniquely
defined if $R$ is not an integral domain.
Let $h$ be a non-constant
polynomial in a univariate polynomial ring $K[x]$ over the
field $K$ and 
\[ h=lc(h)\cdot \prod_{m=1}^r p_m^{i_m} \]
a factorization into irreducible monic factors. The squarefree form
of $h$ is the polynomial $\prod_{m=1}^r p_m$, denoted by ${\em squarefree}(h)$.
Furthermore, ${\em squarefree}(h):=h$ for every $h\in K$.


\smallskip
We first construct a 
set $\bar{S}$ of finite subsets of $R[x]$ and a function
$\overline{Rep}$ from $\bar{S}$ to the set of radicals in $R[x]$:
we define $\bar{S}$ as the union
\[ S~\cup~\bigcup_{C\in S} \{C\cup\{g\}\mid g\in R[x]\setminus R \hbox{ with } 
lc(g)\notin P \hbox{ for every } P\in ap(C)\}
\]
and
\[
\begin{array}{llll}
\hbox{for } B\in S: & \overline{Rep}(B) & := & 
\{f\in R[x]\mid f^P=0 \hbox{ for every } P\in ap(B)\},   \\
\hbox{for } B\in \bar{S}\setminus S: & \overline{Rep}(B) & := & 
\{f\in R[x]\mid {\em squarefree}(g^P) \hbox{ divides } f^P \hbox{ in } K(P)[x]
\\
& & & \hbox{ for every } P\in ap(B\cap R)\},\ \ \  
\hbox{where } \{g\}=B\setminus R.
\end{array}
\]

For proving that $\overline{Rep}(B)$ is a radical for every $B\in \bar{S}$
we need the following lemma.

\medskip
\begin{lemma} Let $I$ be an ideal in $R[x]$. Then the following three 
conditions are equivalent.

\smallskip
\noindent
{\bf (a)} $I$ is a prime ideal in $R[x]$.

\noindent
{\bf (b)} $I\cap R$ is prime in $R$, $J$ is prime in 
$K(I\cap R)[x]$ and $I^{I\cap R}=J\cap (R/I\cap R)[x]$, 
where $J$ is the ideal in $K(I\cap R)[x]$ 
generated by $I^{I\cap R}$.

\noindent
{\bf (c)} $I\cap R$ is prime in $R$ and there exists a polynomial 
$q\in K(I\cap R)[x]$
which is either irreducible over $K(I\cap R)$ or zero and 

\smallskip
\centerline{for every $f\in R[x]$:~~
$f\in I$~ iff~ $f^{I\cap R}\in \langle\{q\}\rangle$.} 
\end{lemma}  

\noindent
{\bf Proof:} {\bf (a)} $\Leftrightarrow$ {\bf (b)}: 
Since 
\begin{equation}
I^{I\cap R}\cap (R/I\cap R)=\{0\}, \label{72:1}
\end{equation}
the equivalence of 
{\bf (a)} and {\bf (b)}
follows from Lemma 4.1 and Lemma 4.2 in 
\cite{GTZ88}.

\smallskip
\noindent
{\bf (b)} $\Rightarrow$ {\bf (c)}: 
Let $q\in K(I\cap R)[x]$ be the polynomial that generates $J$. From (\ref{72:1}) 
we obtain
$I^{I\cap R}\not= (R/I\cap R)[x]$ and therefore $J\not= K(I\cap R)[x]$. Hence,
$q$ is either irreducible or zero. Let $f\in R[x]$. Then
\[ 
f\in I~~~~\hbox{iff}~~~~f^{I\cap R}\in I^{I\cap R}~~~~
\hbox{iff}~~~~
f^{I\cap R}\in J~~~~
\hbox{iff}~~~~
f^{I\cap R}\in \langle\{q\}\rangle.
\]

\noindent
{\bf (c)} $\Rightarrow$ {\bf (b)}: 
$J$ is prime because $q$ generates $J$ and $q$ is irreducible or zero.
Let $f$ be a polynomial in $R[x]$ 
with $f^{I\cap R}\in J$. Then $f^{I\cap R}\in 
\langle\{q\}\rangle$
and therefore $f$ is an element of $I$ and 
$f^{I\cap R}\in I^{I\cap R}.\ \ \Box$

\medskip
\begin{lemma} Let $B\in\bar{S}$. Then $\overline{Rep}(B)$ is a radical and
\[
\begin{array}{llll} 
height(\overline{Rep}(B)) & = & height(Rep(B)) & \hbox{ if } B\in S, \\
height(\overline{Rep}(B)) & = & height(Rep(B\cap R))+1 & 
\hbox{ if } B\notin S. 
\end{array}
\]
If $Rep(B\cap R)$ is unmixed then $\overline{Rep}(B)$ is unmixed.
\end{lemma}
{\bf Proof:} 
Let $P_1,\ldots,P_r$ be the associated prime ideals of $Rep(B\cap R)$.
If $B\in S$ then $\overline{Rep}(B)$ is the extension ideal $Rep(B)\, R[x]$
and therefore a radical. The ideals
$P_1\, R[x],\ldots,$ $P_r\, R[x]$ are the associated prime ideals
of $\overline{Rep}(B)$. By \cite[Theorem 149]{Kapl70}, 
\[ height(\overline{Rep}(B))=height(Rep(B)). \]
Therefore, if $Rep(B\cap R)$ is unmixed then $\overline{Rep}(B)$ is unmixed.

Now assume that $B=C\cup\{g\}$ for
some $C\in S$ and $g\in R[x]\setminus R$ with
$lc(g)\notin P_i$ for every $i\in\{1,\ldots,r\}$.
For $i\in\{1,\ldots,r\}$ let 
\[ g^{P_i}=lc(g^{P_i})\cdot\prod_{j=1}^{l_i} q_{ij}^{k_{ij}} \]
be
a factorization of $g^{P_i}$ in $K(P_i)[x]$. By the previous lemma, the set
\[ P_{ij}:=\{f\in R[x]\mid q_{ij} \hbox{ divides } f^{P_i} \hbox{ in }
K(P_i)[x]\} \] 
is a prime ideal 
for every $j\in\{1,\ldots,l_i\}$. Obviously, 
$\overline{Rep}(B)=\bigcap P_{ij}$ and therefore $\overline{Rep}(B)$
is a radical.
Since 
for every associated prime ideal $P$ of $\overline{Rep}(B)$ 
there exists an $i\in\{1,\ldots,r\}$ with 
\[ P\cap R=P_i\ \ \  \hbox{ and }\ \ \ 
P\not= P_i\, R[x] \]
it follows from \cite[Theorem 149]{Kapl70} that 
\[ height(\overline{Rep}(B))=height(Rep(B\cap R))+1 \] 
and $\overline{Rep}(B)$ is unmixed if $Rep(B\cap R)$ is unmixed.\ \ $\Box$


\bigskip
For an element $B$ of $\bar{S}$ let $\overline{ap}(B)$ denote the set of 
associated prime ideals
of the radical $\overline{Rep}(B)$. 

\smallskip
We now come to the construction of the fundamental computational tool: 
an algorithm for computing gcd's modulo radicals.

\vskip .8cm
${\bf ggcd}(C,F)$
\begin{description}
\item[Input:] $C$, an element of $S$,              
                     
$F=\{f_1,\ldots,f_k\}$, a finite non-empty subset of $R[x]$.
\item[Output:] $\{(C_1,g_1),\ldots,(C_l,g_l)\}$, where
$C_1,\ldots,C_l\in S$ with $ap(C)=\bigcup_{i=1}^l ap(C_i)$
and $g_1,\ldots,g_l\in R[x]$ such that 
for every $i\in\{1,\ldots,l\}$ and every $P\in ap(C_i)$:
\begin{enumerate}
\item $g_i^P$
is the gcd of $f_1^P,\ldots,f_k^P$ in $K(P)[x]$
(up to a multiplicative constant),
\item if $g_i\not=0$ then $lc(g_i)\notin P$,
\item $g_i\in\langle Rep(C_i)\cup F\rangle$.
\end{enumerate}
\end{description}

\vskip .5cm  
{\bf if} $F=\{0\}$ {\bf then}  

\hskip 1cm                           
$O:=\{(C,0)\}$

{\bf else}

\hskip 1cm
$f:=$ a non-zero element in $F$ with minimal degree in $x$

\hskip 1cm
$F':=F\setminus\{f\}$

\hskip 1cm
$(M',M''):={\bf split}_R(C,lc(f))$

\hskip 1cm
$h:=f-lc(f)\cdot x^{deg(f)}$

\hskip 1cm
$F'':=\{prem(g,f)\mid g\in F'\}$

\hskip 1cm
{\bf if} $F''\subseteq\{0\}$ {\bf then}

\hskip 2cm
$O:=\bigcup_{B'\in M'}{\bf ggcd}(B',F'\cup\{h\})\cup
\bigcup_{B''\in M''}\{(B'',f)\}$


\hskip 1cm
{\bf else}

\hskip 2cm
$O:=\bigcup_{B'\in M'}{\bf ggcd}(B',F'\cup\{h\})\cup
\bigcup_{B''\in M''}{\bf ggcd}(B'',F''\cup\{f\})$

\hskip 1cm
{\bf end}

{\bf end}

${\bf return}(O)$

\vskip .5cm
\noindent
{\em Proof of termination and correctness of {\bf ggcd}:}
Let $G$ be a finite non-empty subset of $R[x]$. Define
\[ sumdeg(G):=\sum_{g\in G} (deg(g)+1). \]

Let $C$ and $F$ be sets which satisfy the input specification. 
We will prove termination and correctness by induction on $sumdeg(F)$.

>From $sumdeg(F)=0$ we obtain
$F=\{0\}$
and therefore termination and correctness are obvious.

Let $sumdeg(F)>0$. Obviously, $sumdeg(F'\cup\{h\})<sumdeg(F)$. Furthermore,
if $F''\not\subseteq\{0\}$ then $sumdeg(F''\cup\{f\})<sumdeg(F)$. Hence,
the termination of {\bf ggcd} follows from the induction hypothesis.

The equality $ap(C)=\bigcup_{i=1}^l ap(C_i)$ and condition 2 
in the specification of {\bf ggcd} immediately follow
from the specification of ${\bf split}_R$ and the induction hypothesis.   

Let $(C_i,g_i)$ be an element of the output set and $P\in ap(C_i)$.

Assume that 
there exists a
$B'\in M'$ with $(C_i,g_i)\in {\bf ggcd}(B',F'\cup\{h\})$. 
By the induction hypothesis, $P\in ap(B')$ and therefore $lc(f)\in P$
by the specification of ${\bf split}_R$. Hence,
$h^P=f^P$ and    
condition 1 follows from the induction hypothesis. Since
$lc(f)\in Rep(C_i)$, the polynomial $h$ is in the ideal generated by
$Rep(C_i)\cup F$. Thus, condition 3 follows from the induction hypothesis.

If there exists a
$B''\in M''$ with $(B'',f)=(C_i,g_i)$ then conditions 1 and 3
are obviously satisfied. Otherwise, there exists a
$B''\in M''$ with
$(C_i,g_i)\in {\bf ggcd}(B'',F''\cup\{f\})$. 
By the induction hypothesis, $P\in ap(B'')$ and therefore $lc(f)\notin P$
by the specification of ${\bf split}_R$. Therefore,
the polynomials in the set $\{g^P\mid g\in F\}$ and the 
polynomials in the set $\{g^P\mid g\in F''\cup\{f\}\}$ have the same gcd
and condition 1 follows from the induction hypothesis.
Condition 3 follows 
from the fact that $F''\cup\{f\}$ is a subset of $\langle F\rangle$
and 
the induction hypothesis.\ \ $\Box$




\bigskip
Using this algorithm we construct ${\bf decompose}_{R[x]}$.





\bigskip
${\bf decompose}_{R[x]}(F)$
\begin{description}
\item[Input:] $F$, a finite non-empty subset of $R[x]$.
\item[Output:] $\{C_1,\ldots,C_r\}$, a subset of $\bar{S}$ with
$\sqrt{F}=\bigcap_{i=1}^r \overline{Rep}(C_i)$. 
\end{description}


\vskip .5cm
$M:={\bf decompose}_R(F\cap R)$

{\bf forall} $C\in M$ {\bf do}

\hskip 1cm
$\{(C_1,g_1),\ldots,(C_k,g_k)\}:={\bf ggcd}(C,F)$

\hskip 1cm
$J_C:=\{i\in\{1,\ldots,k\}\mid g_i\not= 0\}$

\hskip 1cm
$O_C:=\{C_i\mid i\in\{1,\ldots,k\}\setminus J_C\}\cup$ 

\hskip 2.1cm
$\{C_i\cup\{g_i\}\mid i\in\{1,\ldots,k\},~g_i\notin R\}\cup$ 

\hskip 2.1cm
$\bigcup_{i\in J_C} {\bf decompose}_{R[x]}(F\cup\{g_i,lc(g_i)\})$

{\bf end}

${\bf return}(\bigcup_{C\in M} O_C)$


\vskip .5cm
\noindent
{\em Proof of termination of ${\bf decompose}_{R[x]}$:}
Let $F$ satisfy the input specification and let $C\in M$.  
It follows from the specification of {\bf ggcd} that
for every $i\in J_C$ the leading coefficient of $g_i$ 
is not in $Rep(C_i)$ and therefore not in $\langle F\cap R\rangle$. 
Since $R$ is Noetherian ${\bf decompose}_{R[x]}$ terminates.\ \ $\Box$

\medskip
For the ideal $I\subseteq R[x]$
and the polynomial $f\in  R[x]$ we define
\[ I:f^{\infty}~:=~ \{g\in R[x]\mid f^m\cdot g\in I \hbox{ for some 
natural number } m\}. \]
It is well-known that 
\begin{equation}
\sqrt{I}=\sqrt{I:f^{\infty}}\cap \sqrt{I\cup\{f\}}. \label{276:1}
\end{equation} 
We will now show that the correctness of ${\bf decompose}_{R[x]}$
is based on this fundamental decomposition formula. 

\medskip
\begin{lemma}
Let $C\in S$ and $g\in R[x]$ such that $C\cup\{g\}\in \bar{S}$. Then
\[ \sqrt{\langle Rep(C)\cup\{g\}\rangle :lc(g)^{\infty}}
=\overline{Rep}(C\cup\{g\}). \]
If $g^P\in K(P)[x]$ is squarefree for every $P\in ap(C)$ then
\[ \langle Rep(C)\cup\{g\}\rangle :lc(g)^{\infty} =
\overline{Rep}(C\cup\{g\}). \]
\end{lemma}
{\bf Proof:}
Let $f\in R[x]$. If $f\in \langle Rep(C)\cup\{g\}\rangle :lc(g)^{\infty}$ 
then $g^P$ divides $f^P$ 
in $K(P)[x]$ for every $P\in ap(C)$
and therefore $f\in\overline{Rep}(C\cup\{g\})$. Since 
$\overline{Rep}(C\cup\{g\})$ is a radical,
\begin{equation} 
\sqrt{\langle Rep(C)\cup\{g\}\rangle :lc(g)^{\infty}}
\subseteq\overline{Rep}(C\cup\{g\}). \label{234:1}
\end{equation}
On the other hand, if $f\in \overline{Rep}(C\cup\{g\})$ then 
there exists a natural number $m$ such that $g^P$ divides $(f^m)^P$
for every $P\in ap(C)$. Thus, $prem(f^m,g)^P=0$ 
for every $P\in ap(C)$ and therefore
$prem(f^m,g)\in \overline{Rep}(C)$
and $f^m\in \langle Rep(C)\cup\{g\}\rangle :lc(g)^{\infty}$. 
Together with (\ref{234:1})
this completes the proof of the first equality.

\smallskip
If $g^P$ is squarefree for every $P\in ap(C)$
we can choose $m$ as 1 and the second equality immediately follows.\ \ $\Box$


\medskip
\noindent
{\em Proof of correctness of ${\bf decompose}_{R[x]}$:}
Let $O$ be the output set with input $F$. 
We will show correctness by induction.

\smallskip
\noindent
{\em Induction basis:} $\langle F\cap R\rangle =R$. 
Then the output set $O$ is empty
and correctness is obvious.

\smallskip
\noindent
{\em Induction step:} $\langle F\cap R\rangle\not= R$. It follows from the
specification of {\bf ggcd}, the definition of $\overline{Rep}$
and the induction hypothesis that

\[ \sqrt{F}\subseteq \bigcap_{A\in O} \overline{Rep}(A). \]
It remains to show that for every prime ideal $P$ with $\sqrt{F}\subseteq P$ 
\begin{equation}
\hbox{there exists
an } A\in O \hbox{ with } \overline{Rep}(A)\subseteq P. \label{185:1a}
\end{equation}
Obviously, there exists a
$C\in M$ and an $i\in\{1,\ldots,k\}$ with $Rep(C_i)\cup\{g_i\}\subseteq P$,
where $\{(C_1,g_1),\ldots,(C_k,g_k)\}:={\bf ggcd}(C,F)$.
If $g_i=0$ then (\ref{185:1a}) is obviously satisfied.  
Otherwise, by (\ref{276:1}),
\[ \sqrt{I}=\sqrt{I :lc(g_i)^{\infty}}\cap \sqrt{I\cup\{lc(g_i)\}}, \]
where $I:=\langle Rep(C_i)\cup\{g_i\}\rangle$.
Therefore, by Lemma 3,
\[  \overline{Rep}(C\cup\{g_i\})\subseteq P\ \ \hbox{ or }\ \ 
lc(g_i)\in P. \]
In the second case (\ref{185:1a}) follows from the induction hypothesis.
\ \ $\Box$




\bigskip
It remains to construct the algorithm {\bf split}$_{R[x]}$. 
Let $K$ be a field, $f,g\in K[x]$ with $f\not= 0$ and 
\[ f=lc(f)\cdot\prod_{m=1}^r p_m^{i_m} \]
a factorization into irreducible monic factors. Define 
\[ M:=\{m\in\{1,\ldots,r\}\mid p_m \hbox{ does not divide } g\}, \]
\[ h:=\prod_{m\in M} p_m^{i_m}\ \hbox{ if } M\not=\emptyset\ \ \ \ 
\hbox{and}\ \ \ \ h:=1\ \hbox{ if } M=\emptyset . \]
Note that $h$ and $g$ are relatively prime and that $h$ is the 
biggest factor of $f$ with this property. We denote $h$
by $rpf(f,g)$.




\vskip .7cm
${\bf relatively\_prime}(C,f,g)$
\begin{description}
\item[Input:] $C$, an element of $S$,
 
$f,g$, polynomials in $R[x]$ such that $f\not= 0$ and $lc(f)\notin P$
for every 
$P\in ap(C)$.
\item[Output:] $\{(C_1,f_1),\ldots,(C_s,f_s)\}$, where $C_1,\ldots,C_s\in S$
with $ap(C)=\bigcup_{i=1}^s ap(C_i)$
and for every 
$i\in\{1,\ldots,s\}$
and $P\in ap(C_i)$ and some
non-zero constant $c\in K(P)$
\[ f_i^P=c\cdot rpf(f^P,g^P)\ \ \hbox{ and }\ \ lc(f_i)\notin P. \]
\end{description}

\vskip .5cm
$\{(D_1,g_1),\ldots,(D_r,g_r)\}:={\bf ggcd}(C,\{f,g\})$

$J:=\{j\in\{1,\ldots,r\}\mid g_j\notin R\}$

$O:=\{(D_j,f)\mid j\in\{1,\ldots,r\}\setminus J\}\cup\bigcup_{j\in J}
{\bf relatively\_prime}(D_j,pquo(f,g_j),g)$

${\bf return}(O)$

\vskip .5cm
\noindent
{\em Proof of termination and correctness of 
{\bf relatively\_prime}}:
Let $C,f,g$ satisfy the input specification and let
$(C_i,f_i)$ be an element of the output $\{(C_1,f_1),\ldots,
(C_s,f_s)\}$ of 
{\bf relatively\_prime}. We do the proof
by induction on $deg(f)$. 

If $deg(f)=0$ termination and correctness immediately
follow from
the specification of {\bf ggcd}.

Let $deg(f)>0$. Obviously, for every $j\in J$ and $P\in ap(D_j)$
\[ lc(pquo(f,g_j))\notin P\ \ \hbox{ and }\ \ deg(f)>deg(pquo(f,g_j)). \]
Therefore, $D_j,pquo(f,g_j),g$ satisfy the input specification of 
{\bf relatively\_prime} and the algorithm terminates.
 
It immediately follows from the
specification of {\bf ggcd} that $ap(C)=\bigcup_{j=1}^s
ap(C_j)$ and $lc(f_i)\notin P$ for every $P\in ap(C_i)$.
If $(C_i,f_i)=(D_j,f)$
for some $j\in\{1,\ldots,r\}\setminus J$ 
then $g_j\in R$. Therefore, $f^P$ and $g^P$ are relatively
prime for every $P\in ap(C_i)$ and correctness is obvious.
Otherwise, there exists
a $j\in J$ such that 
$(C_i,f_i)$ is an element of the output of 
{\bf relatively\_prime} with input 
$D_j,pquo(f,g_j),g$. By definition of $g_j$,
\[ rpf(f^P,g^P)=rpf(pquo(f,g_j)^P,g^P)\ \ \hbox{ for every }
P\in ap(D_j). \]
Therefore correctness follows from the induction hypothesis.
\ \ $\Box$

\bigskip
Now we can construct the algorithm {\bf split}$_{R[x]}$.

\vskip .7cm
{\bf split}$_{R[x]}(C,g)$
\begin{description}
\item[Input:] $C$, an element of $\bar{S}$,
 
$f$, a polynomial in $R[x]$.
\item[Output:] $(\{B_1,\ldots,B_r\},\{C_1,\ldots,C_s\})$, a pair of
subsets of $\bar{S}$ such that 
\begin{equation}
\bigcup_{i=1}^r \overline{ap}(B_i)=
\{P\in \overline{ap}(C)\mid f\in P\},~~
\bigcup_{i=1}^s \overline{ap}(C_i)=
\{P\in \overline{ap}(C)\mid f\notin P\}. \label{2411:1}
\end{equation}
\end{description}

\vskip .5cm
$\{(D_1,g_1),\ldots,(D_m,g_m)\}:={\bf ggcd}(C\cap R,(C\setminus R)\cup\{f\})$
 
{\bf if} $C\subseteq R$ {\bf then}
 
\hskip 1cm
$O_1:=\{D_j\mid j\in\{1,\ldots,m\} \hbox{ and } g_j=0\}$

\hskip 1cm
$O_2:=\{D_j\mid j\in\{1,\ldots,m\} \hbox{ and } g_j\not= 0\}$
 
{\bf else}
 
\hskip 1cm
$O_1:=\{D_j\cup\{g_j\}\mid j\in \{1,\ldots,m\} \hbox{ and } g_j
\notin R\}$

\hskip 1cm
$g:=$ the only element in $C\setminus R$

\hskip 1cm
$\{(E_1,h_1),\ldots,(E_k,h_k)\}:={\bf relatively\_prime}(C\cap R,g,f)$
 
\hskip 1cm
$O_2:=\{E_j\cup\{h_j\}\mid j\in \{1,\ldots,k\} \hbox{ and }
h_k\notin R\}$

{\bf end}

${\bf return}((O_1,O_2))$


\vskip .5cm
\noindent
{\em Proof of termination and correctness of ${\bf split}_{R[x]}$:}
Since ${\bf split}_{R[x]}$ obviously terminates it remains to show its 
correctness.
Let $C$ and $f$ satisfy the input specification and let
$(\{B_1,\ldots,B_r\},\{C_1,\ldots,C_s\})$ be the output 
of ${\bf split}_{R[x]}$ with input $C$ and
$f$. It immediately follows from the specifications of {\bf ggcd}
and {\bf relatively\_prime} that
$\{B_1,\ldots,B_r\}$ and $\{C_1,\ldots,C_s\}$ are subsets of $\bar{S}$. 
Let $P$ be
a prime ideal in $R[x]$.

 
\smallskip
\noindent
{\em Case:} $C\subseteq R$.

\[ 
\begin{array}{c}
P\in \overline{ap}(B_i) \hbox{ for some } i\in\{1,\ldots,r\} \\
\hbox{iff} \\
P=(P\cap R)\, R[x]
\hbox{ and } P\cap R\in ap(C) \hbox{ and } f^{P\cap R}=0 \\
\hbox{iff} \\
P\in \overline{ap}(C) \hbox{ and } f\in P.
\end{array}
\]  
The right equation in (\ref{2411:1}) can be shown in the same way.

\medskip
\noindent
{\em Case:} $C\not\subseteq R$.
 
\smallskip
Denote the element of $C\setminus R$ by $g$ and the set $\{j\in\{1,\ldots,m\}
\mid g_j\notin R\}$ by $J$.

\smallskip 
\[ 
\begin{array}{c}
P\in \overline{ap}(B_i) \hbox{ for some } i\in\{1,\ldots,r\} \\
\hbox{iff}\\
P\in \overline{ap}(D_j\cup\{g_j\}) \hbox{ for some } 
j\in J\\
\hbox{iff}\\
\hbox{there exists a $j\in J$ and an 
irreducible factor
$q\in K(P\cap R)[x]$ of ${g_j}^{P\cap R}$ such that } \\
P=\{h\in R[x]\mid 
q \hbox{ divides } h^{P\cap R}\} \hbox{ and } P\cap R\in ap(D_j) \\
\hbox{iff}\\
\hbox{there exists an 
irreducible $q\in K(P\cap R)[x]$ which divides $g^{P\cap R}$ and $
f^{P\cap R}$,} \\
P=\{h\in R[x]\mid 
q \hbox{ divides } h^{P\cap R}\} \hbox{ and } P\cap R\in ap(C\cap R) \\
\hbox{iff}\\
P\in \overline{ap}(C) \hbox{ and } f\in P.
\end{array}
\]  
The right equation 
in (\ref{2411:1}) can be shown in the same way.\ \ $\Box$



\section{Application to geometry theorem proving}

We construct a system of unmixed representations 
$(S,Rep,{\bf decompose}_K,{\bf split}_K)$ in the field $K$:
\[ S:=\{\emptyset\},\ \ \ Rep(\emptyset):=\{0\}, \]
${\bf decompose}_K$ returns $\{\emptyset\}$ with input $\{0\}$ and 
$\emptyset$ otherwise and ${\bf split}_K(\emptyset,a)$ is 
$(\{\emptyset\},\emptyset)$ if $a=0$ and $(\emptyset,\{\emptyset\})$
otherwise. Using the constructions in the previous section we obtain
a system of unmixed representations
$(\bar{S},\overline{Rep},{\bf decompose}_R,{\bf split}_R)$ in 
$R:=K[x_1,\ldots,x_n]$.
Note that every $C\in\bar{S}$ is a triangular set, i.e. for every 
$i\in\{1,\ldots,n\}$ there exists at most one polynomial in 
$C\cap (K[x_1,\ldots,x_i]\setminus K[x_1,\ldots,x_{i-1}])$. Furthermore
the cardinality of $C\cap K[x_1,\ldots,x_i]$ is the height of 
$\overline{Rep}(C)\cap K[x_1,\ldots,x_i]$ and therefore 
\[ \overline{Rep}(C)\cap K[x_1,\ldots,x_i]=\{0\}\ \ \hbox{ iff }\ \ 
C\cap K[x_1,\ldots,x_i]=\emptyset. \]


\smallskip
We now illustrate the application of the algorithms {\bf decompose} and 
{\bf split} to geometry theorem proving by means of 

\bigskip 
{\bf Apollonios' Circle Theorem:} {\em The altitude pedal of the hypotenuse
of a right-angled triangle and the midpoints of the three sides of the
triangle lie on a circle.}

\medskip
We use the algebraic formulation given in \cite{Buch87}. We
have 8 hypotheses polynomials $h_1,\ldots,h_8$ in 
$R:={\bf Q}[x_1,x_2,\ldots,x_{10}]$: 
\[
\begin{array}{ll}
h_1:=2x_3-x_1, & ~~~~
h_5:=(x_7-x_3)^2+x_8^2-(x_7-x_4)^2-(x_8-x_5)^2, \\
h_2:=2x_4-x_1, & ~~~~
h_6:=(x_7-x_3)^2+x_8^2-(x_8-x_6)^2-x_7^2, \\
h_3:=2x_5-x_2, & ~~~~
h_7:=(x_9-x_1)x_2+x_1x_{10}, \\
h_4:=2x_6-x_2, & ~~~~
h_8:=-x_1x_9+x_2x_{10}. 
\end{array}
\]
The conclusion is
\[ c:=(x_7-x_3)^2+x_8^2-(x_7-x_9)^2-(x_8-x_{10})^2. \]

The set of independent variables is $\{x_1,x_2\}$.

We have to compute 
${\bf decompose}_R(\{h_1,\ldots,h_8\})$. The output set consists of
4 subsets of ${\bf Q}[x_1,\ldots,x_{10}]$:

\smallskip
$C_1~~:=~~\{\, x_1 x_{10}+ x_2 x_9- x_2 x_1,~~ - x_1^2 x_9- x_2
^2 x_9+ x_2^2 x_1,~~ 4 x_8- x_2,~~ -4 x_7+ x_1,$

~~~~~~~~~~~~~~~$2 x_6- x_2,~~ 2 x_5- x_2,~~ 2 x_4- x_1,~~ 2 x_3- x_1\,\}$,

\smallskip
$C_2~~:=~~\{\, x_{10},~~ x_9,~~ 4 x_8-
 x_2,~~ 2 x_6- x_2,~~ 2 x_5- x_2,~~  x_4,~~  x_3,~~  x_1\,\}$,

\smallskip
$C_3~~:=~~ \{\, x_{10},~~ x_9,~~ -4 x_7+ x_1,~~  x_6,~~  x_5,~~ 2 x_4- x_1,~~ 2 x_3- x_1,~~  x_2\,\}$,

\smallskip
$C_4~~:=~~ \{\, x_6,~~  x_5,~~  x_4,~~  x_3,~~ 
 x_2,~~  x_1\,\}$.

\medskip
Only $C_1$ does not contain an element of ${\bf Q}[x_1,x_2]$. Thus
we can check whether the Apollonios' Circle Theorem is true by
computing ${\bf split}_R(C_1,c)$. It turns out that $c$ vanishes on the 
variety of $\overline{Rep}(C_1)$. Therefore
Apollonios' Circle Theorem is true and the polynomial $x_1x_2$
is a nondegeneracy condition, because $x_1$ is in $C_2$ and $C_4$ and
$x_2$ is in $C_3$.

An alternative strategy for deciding the correctness of a geometrical 
statement
is based on Rabinowitsch's trick: we add the negated conclusion to the
hypotheses polynomials and use this enlarged set as input for 
${\bf decompose}$. It is easy to see \cite{Kalk92b} that 
the geometrical statement is true if and only if every element
$B_i$ of the output set $\{B_1,\ldots,B_r\}$ contains a polynomial $g_i\in
K[x_1,\ldots,x_t]$. In this case the product $\prod_{i=1}^r g_i$ is a
nondegeneracy condition. Therefore, for proving Apollonios' Circle Theorem
we have to compute 
${\bf decompose}_{R[x_{11}]}(\{h_1,\ldots,h_8,cx_{11}-1\})$, 
where $x_{11}$ is a new
variable. The output set only contains
$C:=C_4\cup\{cx_{11}-1\}$.
Since $C\cap {\bf Q}[x_1,x_2]=\{x_1,x_2\}$, 
Apollonios' Circle Theorem is true and
$x_1$ and $x_2$ are both nondegeneracy conditions.

\bigskip
Sometimes it is important to find the simplest nondegeneracy 
condition with respect to some criterion. Our approach can be used
for constructing the simplest nondegeneracy condition with
respect to a lexicographical
degree ordering. More precisely, let $D\subseteq
K[x_1,\ldots,x_t]\setminus\{0\}$ be the set of
nondegeneracy conditions, i.e. $d\in D$ iff
\[
(\forall a\in {\bar K}^n) ~[h_1(a)=\ldots =h_m(a)=0\,\wedge\, d(a)\not= 0 
~\Rightarrow ~c(a)=0], \]
and define the following relation on $K[x_1,\ldots,x_t]$: for $f,g\in 
K[x_1,\ldots,x_t]$ we have $f\prec g$ if for some $i\in\{1,\ldots,t\}$
the degree of $f$ in $x_i$ is smaller than the degree of $g$ in 
$x_i$ and $f$ and $g$ have the same degree in each of the variables 
$x_{i+1},\ldots,x_t$.

For presenting an algorithm which computes
a minimal nondegeneracy condition with respect to $\prec$ we need the following
definitions.
Let $f$ be a non-constant polynomial in $K[x_1,\ldots,x_t]$
and $i$ the greatest
element of $\{1,\ldots,t\}$ such that $x_i$ actually appears in $f$. Then 
${\em class}(f):=i$ and ${\em primpart}(f)$
denotes the primitive part of $f$ with respect to $x_i$.
Let $C=\{f_1,f_2,\ldots,f_k\}$ be a non-empty triangular set in 
$K[x_1,\ldots,x_t]$ with
the polynomials $f_1,\ldots,f_k$ ordered in such a way
that ${\em class}(f_i)<{\em class}(f_j)$ if $i<j$. We denote $f_1$ by
${\em first}(C)$. 

Let $\{C_1,\ldots,C_l\}:={\bf decompose}_{R[x_{n+1}]}
(\{h_1,\ldots,h_m,cx_{n+1}-1\})$.
We assume that $C_1,\ldots,
C_l$ 
are ordered in such a way that ${\em class}({\em first}(C_i))\geq 
{\em class}({\em first}(C_j))$ 
for $i<j$.
We define 
\[ 
\begin{array}{lll}
d_1 & := & {\em squarefree}({\em primpart}({\em first}(C_1))), \\ 
d_i & := & {\em squarefree}(d_{i-1}\cdot\prod_{j=1}^{k_i} 
{\em primpart}({\em first}(C_{ji}'))),
~~~~~~~~(i=2,\ldots,l)
\end{array}
 \]
where $(A_i,B_i):={\bf split}_{R[x_{n+1}]}(C_i,d_{i-1})$ and
$C_{1i}',\ldots,C_{{k_i}i}'$ are the elements of $B_i$.

\smallskip
It has been proved in \cite{Kalk92b} that
the polynomial $d_l$ is a minimal nondegeneracy condition with respect to
$\prec$ and that two minimal nondegeneracy conditions are identical except 
for a 
multiplicative constant.

\begin{thebibliography}{GTZ88}

\bibitem[Buc87]{Buch87}
B.~Buchberger.
\newblock {Applications of Gr\"obner bases in non-linear computational
  geometry}.
\newblock In {\em Proc. Workshop on Scientific Software}, pages 59--88, IMA,
  Minneapolis, USA, 1987.

\bibitem[CG90]{ChGa90a}
S.C. Chou and X.S. Gao.
\newblock {Ritt-Wu's decomposition algorithm and geometry theorem proving}.
\newblock In {\em Proc. CADE-10}, pages 202--220, Kaiserslautern, Germany,
  1990.

\bibitem[Cho88]{Chou88}
S.C. Chou.
\newblock {\em {Mechanical Geometry Theorem Proving}}.
\newblock D. Reidel Publ. Comp., Dordrecht, 1988.

\bibitem[CS86]{ChSc86}
S.C. Chou and W.F. Schelter.
\newblock {Proving geometry theorems with rewrite rules}.
\newblock {\em J. Automated Reasoning}, 2:253--273, 1986.

\bibitem[GTZ88]{GTZ88}
P.~Gianni, B.~Trager, and G.~Zacharias.
\newblock {Gr\"obner bases and primary decomposition of polynomial ideals}.
\newblock {\em J. Symb. Comp.}, 6(2 \& 3):149--168, 1988.

\bibitem[Kal94]{Kalk93b}
M.~Kalkbrener.
\newblock {Prime decompositions of radicals in polynomial rings}.
\newblock {\em J. Symb. Comp.}, 18:365--372, 1994.

\bibitem[Kal95]{Kalk92b}
M.~Kalkbrener.
\newblock {A generalized Euclidean algorithm for geometry theorem proving}.
\newblock {\em Annals of Math. and Artificial Intelligence}, 13:73--95, 1995.

\bibitem[Kap70]{Kapl70}
I. Kaplansky.
\newblock {\em {Commutative Rings}}.
\newblock Allyn and Bacon, Boston, 1970.

\bibitem[Kap86]{Kapu86a}
D.~Kapur.
\newblock {Geometry theorem proving using Hilbert's Nullstellensatz}.
\newblock In {\em Proc. SYMSAC'86}, pages 202--208, Waterloo, Canada, 1986.

\bibitem[KH85]{KoHu85}
H.P. Ko and M.A. Hussain.
\newblock {A study of Wu's method -- a method to prove certain theorems in
  elementary geometry}.
\newblock In {\em Proc. of 1985 Congressus Numerantium}, 1985.

\bibitem[KS86]{KuSt86b}
B.~Kutzler and S.~Stifter.
\newblock {Automated geometry theorem proving using Buchberger's algorithm}.
\newblock In {\em Proc. SYMSAC'86}, pages 209--214, Waterloo, Canada, 1986.

\bibitem[Kut88]{Kutz88}
B.~Kutzler.
\newblock {\em {Algebraic approaches to automated theorem proving}}.
\newblock PhD thesis, Univ. Linz, RISC, Linz, Austria, 1988.

\bibitem[KW90]{KaWa90}
D.~Kapur and H.K. Wan.
\newblock {Refutational proofs of geometry theorems via characteristic set
  computation}.
\newblock In {\em Proc. ISSAC`90}, pages 277--284, Tokyo, Japan, 1990.

\bibitem[Rit50]{Ritt50}
J.F. Ritt.
\newblock {\em {Differential Algebra}}.
\newblock AMS Colloquium Publications 33, New York, 1950.

\bibitem[Wan95]{Wang92a}
D.~Wang.
\newblock {Elimination procedures for mechanical theorem proving in
  geometries}.
\newblock {\em Annals of Math. and Artificial Intelligence}, 13:1--24, 1995.

\bibitem[Wu78]{Wu78}
W.~Wu.
\newblock {On the decision problem and the mechanization of theorem proving in
  elementary geometry}.
\newblock {\em Scientia Sinica}, 21(2):157--179, 1978.

\bibitem[Wu84]{Wu84}
W.~Wu.
\newblock {Basic principles of mechanical theorem proving in elementary
  geometries}.
\newblock {\em J. Sys. Sci. and Math. Scis}, 4(3):207--235, 1984.

\end{thebibliography}
\end{document}
