Zero Decomposition for Theorem Proving in Geometry

Dongming Wang LIFIA–IMAG, 46, avenue Félix Viallet, 38031 Grenoble Cedex, France

Abstract

Let K be a field of characteristic 0 and K̃ some extension field of K. A polynomial system is a pair [ℙ, ℚ] of sets of polynomials in K[x_{1}, …, x_{n}], with which the zero set

Zero(ℙ/ℚ) = {(x_{1}, …, x_{n}) ∈ K̃^{n}| P (x_{1}, …, x_{n}) = 0, Q(x_{1}, …, x_{n}) ≠ 0, ∀P ∈ ℙ, Q ∈ ℚ}

is of concern. We present two algorithms for decomposing any polynomial system [ℙ, ℚ] into finitely many triangular systems [𝕋_{1}, 𝕌_{1}], …, [𝕋_{e}, 𝕌_{e}] such that

Zero(ℙ/ℚ) = ⋃_{i=1}^{e} Zero(𝕋_{i}/𝕌_{i}).  (I)

To prove a geometric theorem T which may be formulated algebraically in the form

(∀x_{1} ⋯ ∀x_{n}) [H_{1} = 0 ∧ ⋯ ∧ H_{h} = 0 ∧ D_{1} ≠ 0 ∧ ⋯ ∧ D_{d} ≠ 0 ⟹ C = 0] (II)

with H_{i}, D_{j}, C ∈ K[x_{1}, …, x_{n}], we follow Wu’s method by first computing a zero decomposition of the form (I) with ℙ = {H_{1}, …, H_{h}} and ℚ = {D_{1}, …, D_{d}}, and then determining whether C vanishes on Zero(𝕋_{i}/𝕌_{i}) for each i. The latter can be done straightforwardly by successive pseudo-division. In particular, we advocate using irreducible zero decomposition; based on this, a prover has been implemented which can decide whether the above algebraic form (II) of T is true universally or only for some part of the hypothesis configuration defined by Zero(ℙ/ℚ). Determining the latter is of interest not only for ruling out the degenerate cases in which the theorem may be meaningless or false, but also for dealing with such theorems which involve reducibility or whose precise algebraic formulation involves inequalities. We illustrate the performance of our decomposition algorithms, with several examples and in comparison with Ritt-Wu’s, for theorem proving in geometry. Extension of the algorithms for proving theorems in differential geometry is discussed briefly.