Radical decomposition and geometry theorem proving

Michael Kalkbrener Department of Mathematics Swiss Federal Institute of Technology CH-8092 Zurich, Switzerland

1 Introduction

In the late 70’s and early 80’s the work of Wu Wen-tsun [Wu78], [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, [Cho88], [CG90], [KH85], [KW90], [Wan95], [CS86], [Kap86], [KS86]) that the characteristic set method of Ritt and Wu as well as the Gröbner 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:

(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.

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

The reason for the first restriction is that methods like Gröbner 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 [Kut88] 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 K̄ an algebraically closed field which has infinite transcendence degree over K. Let h_{1}, …, h_{m} and c be polynomials in K[x_{1}, …, x_{n}] obtained by translating the hypotheses and conclusion of a geometrical statement into algebraic equations. During this translation process a set X ⊂ {x_{1}, …, x_{n}} of independent variables can be identified. We assume without loss of generality that X = {x_{1}, …, x_{t}}. Now the problem is to decide whether

(∃d ∈ K[x_{1}, …, x_{t}] \ {0})(∀a ∈ K̄^{n}) [h_{1}(a) = … = h_{m}(a) = 0 ∧ d(a) ≠ 0 ⇒ c(a) = 0],

(1)

and, if so, to find such a nondegeneracy condition d.

For a subset F of K[x_{1}, …, x_{n}] the ideal generated by F is denoted by ⟨F ⟩, the radical of ⟨F ⟩ by \sqrt{F} and the variety of F in K̄^{n} by V (F), i.e.

V (F) = {a ∈ K̄^{n} | f(a) = 0 for every f ∈ F }.

Let V ({h_{1}, …, h_{r}}) = V_{1} ∪ … ∪ V_{k} be a decomposition into irreducible varieties. We may assume that c vanishes on V_{i} for i ∈ {1, …, l} but not on V_{j} for j ∈ {l + 1, …, k} for some l ∈ {0, …, k}. Define V′ := ⋃_{i=1}^{l} V_{i} and V′′ := ⋃_{j=l+1}^{k} V_{j}. Obviously, (1) is true if and only if

there exists a non-zero d ∈ K[x_{1}, …, x_{t}] which vanishes on V′′.  (2)

In this case d is a nondegeneracy condition. Hence the correctness of (1) can be decided by decomposing V into V′ ∪V′′ and by deciding (2). Both can be done by means of Gröbner bases and therefore this method is useful for geometry theorem proving ([Kap86], [CS86]): since V′′ = V (I), where I is the ideal ⟨h_{1}, …, h_{m}, cy − 1⟩ ∩ K[x_{1}, …, x_{n}] and y is a new variable, we only have to check whether G∩K[x_{1}, …, x_{t}] = ∅, where G is a Gröbner basis of ⟨h_{1}, …, h_{m}, cy − 1⟩ with respect to a suitable elimination order. Instead of Gröbner bases the prime decomposition algorithm of Ritt and Wu can be used ([Rit50], [Wu84]). Based on elimination by pseudodivision and factorization this algorithm computes for every i ∈ {1, …, 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} ∈ K[x_{1}, …, x_{t}] which vanishes on V_{i}. Hence (2) 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, decompose_{R}, split_{R}) in R consists of

(1) a set S of finite subsets of R,

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

(3) an algorithm decompose_{R} that computes for a finite non-empty subset F of R a subset {C_{1}, …, C_{r}} of S such that

\sqrt{F} = ⋂_{i=1}^{r} Rep(C_{i}),

(4) an algorithm split_{R} that computes for a given A ∈ S and f ∈ R a pair ({B_{1}, …, B_{r}}, {C_{1}, …, C_{s}}) of subsets of S such that

⋃_{i=1}^{r} ap(B_{i}) = {P ∈ ap(A) | f ∈ P } and ⋃_{i=1}^{s} ap(C_{i}) = {P ∈ ap(A) | f ∉ P },

where ap(C) denotes the set of associated prime ideals of Rep(C) for C ∈ S.

Recall that a prime ideal P ≠ R is said to have height h if there exists at least one chain P_{0} ⊂ P_{1} ⊂ … ⊂ 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, decompose_{R}, split_{R}) a system of unmixed resp. prime representations if Rep(A) is unmixed resp. prime for every A ∈ S.

Example 1 Let R be the multivariate polynomial ring K[x_{1}, …, 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 ∈ S. In this case decompose_{R} is the trivial algorithm whose output is equal to its input. As explained above the algorithm split_{R} is based on computing localizations by means of Gröbner 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 split_{R} are defined as above but decompose_{R} is now an algorithm which computes for a finite non-empty subset F of K[x_{1}, …, x_{n}] a finite basis of \sqrt{F} (see [GTZ88], for such an algorithm).

Let S′ be the set of irreducible ascending sets in K[x_{1}, …, x_{n}] (see [Wu84]) and S := S′ ∪ {{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 decompose_{R} is now the prime decomposition algorithm of Ritt [Rit50]. We can decide for every f ∈ K[x_{1}, …, x_{n}] and every prime ideal P ⊂ K[x_{1}, …, x_{n}] given by an irreducible ascending set whether f ∈ P using pseudodivision [Wu84]. Since Rep(A) is prime for every A ∈ S we obtain an algorithm split_{R}. Therefore the set of irreducible ascending sets together with the function Rep and these two algorithms is a system of prime representations.

Our main result is the following theorem.

Theorem 1 If there exists a system of (unmixed) representations in R then there exists a system of (unmixed) representations in R[x_{1}, …, x_{n}].

For a similar result on systems of prime representations we refer to [Kal94].

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 decompose_{R[x_{1},...,x_{n}]} and split_{R[x_{1},...,x_{n}]} is the computation of greatest common divisors of univariate polynomials over extension fields. No factorization or Gröbner 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 (1) but also for constructing simplest nondegeneracy conditions with respect to lexicographical degree orderings.

2 Proof of Theorem 1

Throughout this section let (S, Rep, decompose_{R}, split_{R}) be a system of representations in R. For proving Theorem 1 it suffices to construct a system of representations (S̄, \overline{Rep}, decompose_{R[x]}, split_{R[x]}) in the univariate polynomial ring R[x].

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} | f ∈ 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 ∈ R[x] with g ≠ 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} · f = pquo(f, g) · g + prem(f, g),
deg(pquo(f, g)) < d 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) · ∏_{m=1}^{r} p_{m}^{i_{m}}

a factorization into irreducible monic factors. The squarefree form of h is the polynomial ∏_{m=1}^{r} p_{m}, denoted by squarefree(h). Furthermore, squarefree(h) := h for every h ∈ K.

We first construct a set S̄ of finite subsets of R[x] and a function \overline{Rep} from S̄ to the set of radicals in R[x]: we define S̄ as the union

S ∪ ⋃_{C∈S}{C ∪ {g} | g ∈ R[x] \ R with lc(g) ∉ P for every P ∈ ap(C)}

and

for B ∈ S :  \overline{Rep}(B) := \{f ∈ R[x] | f^{P} = 0 for every P ∈ ap(B)\},
for B ∈ S̄ \ S : \overline{Rep}(B) := \{f ∈ R[x] | squarefree(g^{P}) divides f^{P} in K(P)[x]
for every P ∈ ap(B ∩ R)}, where {g} = B \ R.

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

Lemma 1 Let I be an ideal in R[x]. Then the following three conditions are equivalent.

(a) I is a prime ideal in R[x].

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

(c) I ∩ R is prime in R and there exists a polynomial q ∈ K(I ∩ R)[x] which is either irreducible over K(I ∩ R) or zero and

for every f ∈ R[x]: f ∈ I iff f^{I∩R} ∈ ⟨{q}⟩.

Proof: (a) ⇔ (b): Since

I^{I∩R} ∩ (R/I ∩ R) = {0},  (3)

the equivalence of (a) and (b) follows from Lemma 4.1 and Lemma 4.2 in [GTZ88].

(b) ⇒ (c): Let q ∈ K(I ∩ R)[x] be the polynomial that generates J. From (3) we obtain I^{I∩R} ≠ (R/I ∩ R)[x] and therefore J ≠ K(I ∩ R)[x]. Hence, q is either irreducible or zero. Let f ∈ R[x]. Then

f ∈ I iff f^{I∩R} ∈ I^{I∩R} iff f^{I∩R} ∈ J iff f^{I∩R} ∈ ⟨{q}⟩.

(c) ⇒ (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∩R} ∈ J. Then f^{I∩R} ∈ ⟨{q}⟩ and therefore f is an element of I and f^{I∩R} ∈ I^{I∩R}. □

Lemma 2 Let B ∈ S̄. Then \overline{Rep}(B) is a radical and

\begin{aligned}height(\overline{Rep}(B)) & = & height(Rep(B)) & if B ∈ S, \\ height(\overline{Rep}(B)) & = & height(Rep(B ∩ R)) + 1 & if B ∉ S. \end{aligned}

If Rep(B ∩ R) is unmixed then \overline{Rep}(B) is unmixed.

Proof: Let P_{1}, …, P_{r} be the associated prime ideals of Rep(B ∩ R). If B ∈ S then \overline{Rep}(B) is the extension ideal Rep(B) R[x] and therefore a radical. The ideals P_{1} R[x], …, P_{r} R[x] are the associated prime ideals of \overline{Rep}(B). By [Kap70, Theorem 149],

height(\overline{Rep}(B)) = height(Rep(B)).

Therefore, if Rep(B ∩ R) is unmixed then \overline{Rep}(B) is unmixed.

Now assume that B = C ∪ {g} for some C ∈ S and g ∈ R[x] \ R with lc(g) ∉ P_{i} for every i ∈ {1, …, r}. For i ∈ {1, …, r} let

g^{P_{i}} = lc(g^{P_{i}}) · ∏_{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 ∈ R[x] | q_{ij} divides f^{P_{i}} in K(P_{i})[x]}

is a prime ideal for every j ∈ \{1, …, l_{i}\}. Obviously, \overline{Rep}(B) = ⋂ 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 ∈ {1, …, r} with

P ∩ R = P_{i} and P ≠ P_{i} R[x]

it follows from [Kap70, Theorem 149] that

height(\overline{Rep}(B)) = height(Rep(B ∩ R)) + 1

and \overline{Rep}(B) is unmixed if Rep(B ∩ R) is unmixed. □

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

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

ggcd(C, F)

Input: C, an element of S,

F = {f_{1}, …, f_{k}}, a finite non-empty subset of R[x].

Output: {(C_{1}, g_{1}), …, (C_{l}, g_{l})}, where C_{1}, …, C_{l} ∈ S with ap(C) = ⋃_{i=1}^{l} ap(C_{i}) and g_{1}, …, g_{l} ∈ R[x] such that for every i ∈ {1, …, l} and every P ∈ ap(C_{i}):

1. g_{i}^{P} is the gcd of f_{1}^{P} , …, f_{k}^{P} in K(P)[x] (up to a multiplicative constant),

2. if g_{i} ≠ 0 then lc(g_{i}) ∉ P,

3. g_{i} ∈ ⟨Rep(C_{i}) ∪ F ⟩.

if F = {0} then

O := {(C, 0)} else

f := a non-zero element in F with minimal degree in x F′ := F \ {f} (M′, M′′) := split_{R}(C, lc(f)) h := f − lc(f) · x^{deg(f)} F′′ := {prem(g, f) | g ∈ F′} if F′′ ⊆ {0} then

O := ⋃_{B′∈M′} ggcd(B′, F′ ∪ {h}) ∪ ⋃_{B′′∈M′′}{(B′′, f)} else

O := ⋃_{B′∈M′} ggcd(B′, F′ ∪ {h}) ∪ ⋃_{B′′∈M′′} ggcd(B′′, F′′ ∪ {f}) end

end return(O)

Proof of termination and correctness of ggcd: Let G be a finite non-empty subset of R[x]. Define

sumdeg(G) := ∑_{g∈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′ ∪ {h}) < sumdeg(F). Furthermore, if F′′ ⊈ {0} then sumdeg(F′′ ∪{f}) < sumdeg(F). Hence, the termination of ggcd follows from the induction hypothesis.

The equality ap(C) = ⋃_{i=1}^{l} ap(C_{i}) and condition 2 in the specification of ggcd immediately follow from the specification of split_{R} and the induction hypothesis.

Let (C_{i}, g_{i}) be an element of the output set and P ∈ ap(C_{i}).

Assume that there exists a B′ ∈ M′ with (C_{i}, g_{i}) ∈ ggcd(B′, F′ ∪ {h}). By the induction hypothesis, P ∈ ap(B′) and therefore lc(f) ∈ P by the specification of split_{R}. Hence, h^{P} = f^{P} and condition 1 follows from the induction hypothesis. Since lc(f) ∈ Rep(C_{i}), the polynomial h is in the ideal generated by Rep(C_{i}) ∪ F. Thus, condition 3 follows from the induction hypothesis.

If there exists a B′′ ∈ M′′ with (B′′, f) = (C_{i}, g_{i}) then conditions 1 and 3 are obviously satisfied. Otherwise, there exists a B′′ ∈ M′′ with (C_{i}, g_{i}) ∈ ggcd(B′′, F′′ ∪ {f}). By the induction hypothesis, P ∈ ap(B′′) and therefore lc(f) ∉ P by the specification of split_{R}. Therefore, the polynomials in the set {g^{P} | g ∈ F } and the polynomials in the set {g^{P} | g ∈ F′′ ∪ {f}} have the same gcd and condition 1 follows from the induction hypothesis. Condition 3 follows from the fact that F′′ ∪ {f} is a subset of ⟨F ⟩ and the induction hypothesis. □

Using this algorithm we construct decompose_{R[x]}.

decompose_{R[x]}(F)

Input: F, a finite non-empty subset of R[x].

Output: \{C_{1}, …, C_{r}\}, a subset of S̄ with \sqrt{F} = ⋂_{i=1}^{r} \overline{Rep}(C_{i}).

M := decompose_{R}(F ∩ R)

forall C ∈ M do {(C_{1}, g_{1}), …, (C_{k}, g_{k})} := ggcd(C, F)

J_{C} := {i ∈ {1, …, k} | g_{i} ≠ 0}
O_{C} := {C_{i} | i ∈ {1, …, k} \ J_{C}}∪
{C_{i} ∪ {g_{i}} | i ∈ {1, …, k}, g_{i} ∉ R}∪
⋃_{i∈J_{C}} decompose_{R[x]}(F ∪ {g_{i}, lc(g_{i})})

end

return(⋃_{C∈M} O_{C})

Proof of termination of decompose_{R[x]}: Let F satisfy the input specification and let C ∈ M. It follows from the specification of ggcd that for every i ∈ J_{C} the leading coefficient of g_{i} is not in Rep(C_{i}) and therefore not in ⟨F ∩ R⟩. Since R is Noetherian decompose_{R[x]} terminates. □

For the ideal I ⊆ R[x] and the polynomial f ∈ R[x] we define

I : f^{∞} := {g ∈ R[x] | f^{m} · g ∈ I for some natural number m}.

It is well-known that

\sqrt{I} = \sqrt{I : f^{∞}} ∩ \sqrt{I ∪ \{f\}}.  (4)

We will now show that the correctness of decompose_{R[x]} is based on this fundamental decomposition formula.

Lemma 3 Let C ∈ S and g ∈ R[x] such that C ∪ {g} ∈ S̄. Then

\sqrt{⟨Rep(C) ∪ \{g\}⟩ : lc(g)^{∞}} = \overline{Rep}(C ∪ \{g\}).

If g^{P} ∈ K(P)[x] is squarefree for every P ∈ ap(C) then

⟨Rep(C) ∪ \{g\}⟩ : lc(g)^{∞} = \overline{Rep}(C ∪ \{g\}).

Proof: Let f ∈ R[x]. If f ∈ ⟨Rep(C) ∪ {g}⟩ : lc(g)^{∞} then g^{P} divides f^{P} in K(P)[x] for every P ∈ ap(C) and therefore f ∈ \overline{Rep}(C ∪ \{g\}). Since \overline{Rep}(C ∪ \{g\}) is a radical,

\sqrt{⟨Rep(C) ∪ \{g\}⟩ : lc(g)^{∞}} ⊆ \overline{Rep}(C ∪ \{g\}).  (5)

On the other hand, if f ∈ \overline{Rep}(C ∪ \{g\}) then there exists a natural number m such that g^{P} divides (f^{m})^{P} for every P ∈ ap(C). Thus, prem(f^{m}, g)^{P} = 0 for every P ∈ ap(C) and therefore prem(f^{m}, g) ∈ \overline{Rep}(C) and f^{m} ∈ ⟨Rep(C) ∪ \{g\}⟩ : lc(g)^{∞}. Together with (5) this completes the proof of the first equality.

If g^{P} is squarefree for every P ∈ ap(C) we can choose m as 1 and the second equality immediately follows. □

Proof of correctness of decompose_{R[x]}: Let O be the output set with input F. We will show correctness by induction. Induction basis: ⟨F ∩R⟩ = R. Then the output set O is empty and correctness is obvious. Induction step: ⟨F ∩ R⟩ ≠ R. It follows from the specification of ggcd, the definition of \overline{Rep} and the induction hypothesis that

\sqrt{F} ⊆ ⋂_{A∈O} \overline{Rep}(A).

It remains to show that for every prime ideal P with \sqrt{F} ⊆ P

there exists an A ∈ O with \overline{Rep}(A) ⊆ P.  (6)

Obviously, there exists a C ∈ M and an i ∈ {1, …, k} with Rep(C_{i}) ∪ {g_{i}} ⊆ P, where {(C_{1}, g_{1}), …, (C_{k}, g_{k})} := ggcd(C, F). If g_{i} = 0 then (6) is obviously satisfied. Otherwise, by (4),

\sqrt{I} = \sqrt{I : lc(g_{i})^{∞}} ∩ \sqrt{I ∪ \{lc(g_{i})\}},

where I := ⟨Rep(C_{i}) ∪ {g_{i}}⟩. Therefore, by Lemma 3,

\overline{Rep}(C ∪ \{g_{i}\}) ⊆ P or lc(g_{i}) ∈ P.

In the second case (6) follows from the induction hypothesis. □

It remains to construct the algorithm split_{R[x]}. Let K be a field, f, g ∈ K[x] with f ≠ 0 and

f = lc(f) · ∏_{m=1}^{r} p_{m}^{i_{m}}

a factorization into irreducible monic factors. Define

M := {m ∈ {1, …, r} | p_{m} does not divide g},

h := ∏_{m∈M} p_{m}^{i_{m}} if M ≠ ∅ and h := 1 if M = ∅.

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).

relatively prime(C, f, g)

Input: C, an element of S,

f, g, polynomials in R[x] such that f ≠ 0 and lc(f) ∉ P for every P ∈ ap(C).

Output: {(C_{1}, f_{1}), …, (C_{s}, f_{s})}, where C_{1}, …, C_{s} ∈ S with ap(C) = ⋃_{i=1}^{s} ap(C_{i}) and for every i ∈ {1, …, s} and P ∈ ap(C_{i}) and some non-zero constant c ∈ K(P)

f_{i}^{P} = c · rpf(f^{P} , g^{P}) and lc(f_{i}) ∉ P.

{(D_{1}, g_{1}), …, (D_{r}, g_{r})} := ggcd(C, {f, g})

J := {j ∈ {1, …, r} | g_{j} ∉ R}

O := {(D_{j}, f) | j ∈ {1, …, r} \ J} ∪ ⋃_{j∈J} relatively prime(D_{j}, pquo(f, g_{j}), g)

return(O)

Proof of termination and correctness of 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}), …, (C_{s}, f_{s})} of relatively prime. We do the proof by induction on deg(f).

If deg(f) = 0 termination and correctness immediately follow from the specification of ggcd.

Let deg(f) > 0. Obviously, for every j ∈ J and P ∈ ap(D_{j})

lc(pquo(f, g_{j})) ∉ P and deg(f) > deg(pquo(f, g_{j})).

Therefore, D_{j}, pquo(f, g_{j}), g satisfy the input specification of relatively prime and the algorithm terminates.

It immediately follows from the specification of ggcd that ap(C) = ⋃_{j=1}^{s} ap(C_{j}) and lc(f_{i}) ∉ P for every P ∈ ap(C_{i}). If (C_{i}, f_{i}) = (D_{j}, f) for some j ∈ {1, …, r} \ J then g_{j} ∈ R. Therefore, f^{P} and g^{P} are relatively prime for every P ∈ ap(C_{i}) and correctness is obvious. Otherwise, there exists a j ∈ J such that (C_{i}, f_{i}) is an element of the output of 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}) for every P ∈ ap(D_{j}).

Therefore correctness follows from the induction hypothesis. □

Now we can construct the algorithm split_{R[x]}.

split_{R[x]}(C, g)

Input: C, an element of S̄, f, a polynomial in R[x].

Output: ({B_{1}, …, B_{r}}, {C_{1}, …, C_{s}}), a pair of subsets of S̄ such that

⋃_{i=1}^{r} \overline{ap}(B_{i}) = \{P ∈ \overline{ap}(C) | f ∈ P \}, ⋃_{i=1}^{s} \overline{ap}(C_{i}) = \{P ∈ \overline{ap}(C) | f ∉ P \}. (7)

{(D_{1}, g_{1}), …, (D_{m}, g_{m})} := ggcd(C ∩ R, (C \ R) ∪ {f})

if C ⊆ R then O_{1} := {D_{j} | j ∈ {1, …, m} and g_{j} = 0}

O_{2} := {D_{j} | j ∈ {1, …, m} and g_{j} ≠ 0}

else O_{1} := {D_{j} ∪ {g_{j}} | j ∈ {1, …, m} and g_{j} ∉ R} g := the only element in C \ R {(E_{1}, h_{1}), …, (E_{k}, h_{k})} := relatively prime(C ∩ R, g, f) O_{2} := {E_{j} ∪ {h_{j}} | j ∈ {1, …, k} and h_{k} ∉ R}

end

return((O_{1}, O_{2}))

Proof of termination and correctness of split_{R[x]}: Since split_{R[x]} obviously terminates it remains to show its correctness. Let C and f satisfy the input specification and let ({B_{1}, …, B_{r}}, {C_{1}, …, C_{s}}) be the output of split_{R[x]} with input C and f. It immediately follows from the specifications of ggcd and relatively prime that {B_{1}, …, B_{r}} and {C_{1}, …, C_{s}} are subsets of S̄. Let P be a prime ideal in R[x]. Case: C ⊆ R.

P ∈ \overline{ap}(B_{i}) for some i ∈ \{1, …, r\}

iff P = (P ∩ R) R[x] and P ∩ R ∈ ap(C) and f^{P ∩R} = 0 iff P ∈ \overline{ap}(C) and f ∈ P.

The right equation in (7) can be shown in the same way.

Case: C ⊈ R.

Denote the element of C \ R by g and the set {j ∈ {1, …, m} | g_{j} ∉ R} by J.

P ∈ \overline{ap}(B_{i}) for some i ∈ \{1, …, r\}

iff P ∈ \overline{ap}(D_{j} ∪ \{g_{j}\}) for some j ∈ J iff

there exists a j ∈ J and an irreducible factor q ∈ K(P ∩ R)[x] of g_{j}^{P ∩R} such that

P = {h ∈ R[x] | q divides h^{P ∩R}} and P ∩ R ∈ ap(D_{j}) iff there exists an irreducible q ∈ K(P ∩ R)[x] which divides g^{P ∩R} and f^{P ∩R}, P = {h ∈ R[x] | q divides h^{P ∩R}} and P ∩ R ∈ ap(C ∩ R) iff P ∈ \overline{ap}(C) and f ∈ P.

The right equation in (7) can be shown in the same way. □

3 Application to geometry theorem proving

We construct a system of unmixed representations (S, Rep, decompose_{K}, split_{K}) in the field K:

S := {∅}, Rep(∅) := {0},

decompose_{K} returns {∅} with input {0} and ∅ otherwise and split_{K}(∅, a) is ({∅}, ∅) if a = 0 and (∅, {∅}) otherwise. Using the constructions in the previous section we obtain a system of unmixed representations (S̄, \overline{Rep}, decompose_{R}, split_{R}) in R := K[x_{1}, …, x_{n}]. Note that every C ∈ S̄ is a triangular set, i.e. for every i ∈ {1, …, n} there exists at most one polynomial in C ∩(K[x_{1}, …, x_{i}]\K[x_{1}, …, x_{i−1}]). Furthermore the cardinality of C ∩ K[x_{1}, …, x_{i}] is the height of \overline{Rep}(C) ∩ K[x_{1}, …, x_{i}] and therefore

\overline{Rep}(C) ∩ K[x_{1}, …, x_{i}] = \{0\} iff C ∩ K[x_{1}, …, x_{i}] = ∅.

We now illustrate the application of the algorithms decompose and split to geometry theorem proving by means of

Apollonios’ Circle Theorem: 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.

We use the algebraic formulation given in [Buc87]. We have 8 hypotheses polynomials h_{1}, …, h_{8} in R := Q[x_{1}, x_{2}, …, x_{10}]:

\begin{matrix}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_{1}x_{10}, \\ h_{4} := 2x_{6} − x_{2}, & h_{8} := −x_{1}x_{9} + x_{2}x_{10}. \end{matrix}

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 decompose_{R}({h_{1}, …, h_{8}}). The output set consists of 4 subsets of Q[x_{1}, …, x_{10}]:

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}, 4x_{8} − x_{2}, −4x_{7} + x_{1},

2x_{6} − x_{2}, 2x_{5} − x_{2}, 2x_{4} − x_{1}, 2x_{3} − x_{1} },

C_{2} := { x_{10}, x_{9}, 4x_{8} − x_{2}, 2x_{6} − x_{2}, 2x_{5} − x_{2}, x_{4}, x_{3}, x_{1} },

C_{3} := { x_{10}, x_{9}, −4x_{7} + x_{1}, x_{6}, x_{5}, 2x_{4} − x_{1}, 2x_{3} − x_{1}, x_{2} },

C_{4} := { x_{6}, x_{5}, x_{4}, x_{3}, x_{2}, x_{1} }.

Only C_{1} does not contain an element of Q[x_{1}, x_{2}]. Thus we can check whether the Apollonios’ Circle Theorem is true by computing 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_{1}x_{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 decompose. It is easy to see [Kal95] that the geometrical statement is true if and only if every element B_{i} of the output set {B_{1}, …, B_{r}} contains a polynomial g_{i} ∈ K[x_{1}, …, x_{t}]. In this case the product ∏_{i=1}^{r} g_{i} is a nondegeneracy condition. Therefore, for proving Apollonios’ Circle Theorem we have to compute decompose_{R[x_{11}]}({h_{1}, …, h_{8}, cx_{11} − 1}), where x_{11} is a new variable. The output set only contains C := C_{4} ∪{cx_{11} −1}. Since C ∩Q[x_{1}, x_{2}] = {x_{1}, x_{2}}, Apollonios’ Circle Theorem is true and x_{1} and x_{2} are both nondegeneracy conditions.

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 ⊆ K[x_{1}, …, x_{t}] \ {0} be the set of nondegeneracy conditions, i.e. d ∈ D iff

(∀a ∈ K̄^{n}) [h_{1}(a) = … = h_{m}(a) = 0 ∧ d(a) ≠ 0 ⇒ c(a) = 0],

and define the following relation on K[x_{1}, …, x_{t}]: for f, g ∈ K[x_{1}, …, x_{t}] we have f ≺ g if for some i ∈ {1, …, 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}, …, x_{t}.

For presenting an algorithm which computes a minimal nondegeneracy condition with respect to ≺ we need the following definitions. Let f be a non-constant polynomial in K[x_{1}, …, x_{t}] and i the greatest element of {1, …, t} such that x_{i} actually appears in f. Then class(f) := i and primpart(f) denotes the primitive part of f with respect to x_{i}. Let C = {f_{1}, f_{2}, …, f_{k}} be a non-empty triangular set in K[x_{1}, …, x_{t}] with the polynomials f_{1}, …, f_{k} ordered in such a way that class(f_{i}) < class(f_{j}) if i < j. We denote f_{1} by first(C).

Let {C_{1}, …, C_{l}} := decompose_{R[x_{n+1}]}({h_{1}, …, h_{m}, cx_{n+1} − 1}). We assume that C_{1}, …, C_{l} are ordered in such a way that class(first(C_{i})) ≥ class(first(C_{j})) for i < j. We define

d_{1} := squarefree(primpart(first(C_{1}))),
d_{i} := squarefree(d_{i−1} · ∏_{j=1}^{k_{i}} primpart(first(C′_{ji}))),  (i = 2, …, l)

where (A_{i}, B_{i}) := split_{R[x_{n+1}]}(C_{i}, d_{i−1}) and C′_{1i}, …, C′_{k_{i}i} are the elements of B_{i}.

It has been proved in [Kal95] that the polynomial d_{l} is a minimal nondegeneracy condition with respect to ≺ and that two minimal nondegeneracy conditions are identical except for a multiplicative constant.

References

[Buc87] B. Buchberger. Applications of Gröbner bases in non-linear computational geometry. In Proc. Workshop on Scientific Software, pages 59–88, IMA, Minneapolis, USA, 1987.

[CG90] S.C. Chou and X.S. Gao. Ritt-Wu’s decomposition algorithm and geometry theorem proving. In Proc. CADE-10, pages 202–220, Kaiserslautern, Germany, 1990.

[Cho88] S.C. Chou. Mechanical Geometry Theorem Proving. D. Reidel Publ. Comp., Dordrecht, 1988.

[CS86] S.C. Chou and W.F. Schelter. Proving geometry theorems with rewrite rules. J. Automated Reasoning, 2:253–273, 1986.

[GTZ88] P. Gianni, B. Trager, and G. Zacharias. Gröbner bases and primary decomposition of polynomial ideals. J. Symb. Comp., 6(2 & 3):149–168, 1988.

[Kal94] M. Kalkbrener. Prime decompositions of radicals in polynomial rings. J. Symb. Comp., 18:365–372, 1994.

[Kal95] M. Kalkbrener. A generalized Euclidean algorithm for geometry theorem proving. Annals of Math. and Artificial Intelligence, 13:73–95, 1995.

[Kap70] I. Kaplansky. Commutative Rings. Allyn and Bacon, Boston, 1970.

[Kap86] D. Kapur. Geometry theorem proving using Hilbert’s Nullstellensatz. In Proc. SYMSAC’86, pages 202–208, Waterloo, Canada, 1986.

[KH85] H.P. Ko and M.A. Hussain. A study of Wu’s method – a method to prove certain theorems in elementary geometry. In Proc. of 1985 Congressus Numerantium, 1985.

[KS86] B. Kutzler and S. Stifter. Automated geometry theorem proving using Buchberger’s algorithm. In Proc. SYMSAC’86, pages 209–214, Waterloo, Canada, 1986.

[Kut88] B. Kutzler. Algebraic approaches to automated theorem proving. PhD thesis, Univ. Linz, RISC, Linz, Austria, 1988.

[KW90] D. Kapur and H.K. Wan. Refutational proofs of geometry theorems via characteristic set computation. In Proc. ISSAC‘90, pages 277–284, Tokyo, Japan, 1990.

[Rit50] J.F. Ritt. Differential Algebra. AMS Colloquium Publications 33, New York, 1950.

[Wan95] D. Wang. Elimination procedures for mechanical theorem proving in geometries. Annals of Math. and Artificial Intelligence, 13:1–24, 1995.

[Wu78] W. Wu. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 21(2):157–179, 1978.

[Wu84] W. Wu. Basic principles of mechanical theorem proving in elementary geometries. J. Sys. Sci. and Math. Scis, 4(3):207–235, 1984.