思路

对于几何定理（geometric theorems）的证明，可以通过引入笛卡尔坐标系，然后将前提（hypotheses）和结论（conclusions）描述为关于命题中点的坐标的多项式方程。令 $A, B, C, D, E, F$ 都是实数空间中的点，

线段平行， $\overline{AB} \| \overline{CD}$
线段垂直， $\overline{AB} \perp \overline{CD}$
$A, B, C$ 三点共线（collinear）
距离相等， $A B = C D$
$C$ 落在以 $A$ 为中心 $A B$ 为半径的圆上
$C$ 是 $\overline{AB}$ 的中点
锐角相等， $\angle ABC = \angle DEF$
$\overline{BD}$ 平分角 $\angle ABC$
$\cdots$

这些基本的几何性质，都可以用关于点坐标的多项式来描述。

我们说一个几何定理是可接受的（admissible），如果它的前提和结论都可以被翻译为多项式方程。

给定任意一个几何定理，总有一些点的坐标是任意的（arbitrary），也总有另一些点的坐标是确定的（determined）。定义自变量（independent variables）为 $u_1,\cdots,u_m$ ，定义因变量（dependent variables）为 $x_1,\dots,x_n$ ，那么可接受的几何定理的前提可以描述为一组多项式
$\begin{aligned} h_1(u_1,\cdots,u_m,x_1,\cdots,x_n) &= 0,\\ h_2(u_1,\cdots,u_m,x_1,\cdots,x_n) &= 0,\\ \vdots\\ h_n(u_1,\cdots,u_m,x_1,\cdots,x_n) &= 0.\\ \end{aligned}$
同时，可接受的几何定理的结论可以描述为单个多项式（如果结论包含了一组多项式，也依旧可以一个个地解决）
$g(u_1,\cdots,u_m,x_1,\cdots,x_n) = 0.$

严格遵循

我们说结论 $g$ 严格地遵循（follows strictly）前提 $h_1,\cdots,h_n$ ，如果 $\in \pmb I(V) \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$ ，其中簇 $\pmb V(h_1,\cdots,h_n)$

充分不必要条件：如果 $\in \sqrt{<h_1,\cdots,h_n>}$ ，那么 $g$ 严格遵循 $h_1,\cdots,h_n$

利用 the radical membership algorithm，定义理想
$\bar I = <h_1,\cdots,h_n,1-yg> \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n,y]$
那么 $\in \sqrt{<h_1,\cdots,h_n>} \iff G = \{1\}$ ，这里 $G$ 是 $\bar I$ 的约简Groebner基。

仅当 $\sqrt{<h_1,\cdots,h_n>} = \pmb I(V)$ ，它的逆命题成立。

普遍遵循

然而，上述的严格遵循过于严格，没有考虑“退化”情况（degenerate cases）：令 $\pmb V(h_1,\cdots,h_n)$ ，做簇的最小分解 $U_1 \cup \cdots \cup U_s$ ，某个自由变量 $u_i$ 在某个簇 $U_j$ 上不再自由。例如， $U_2 = \pmb V(x_1,x_2-u_3,u_1)$ ，那么 $u_1 = 0$ 不再能够任意取值。这种退化会使得 $g$ 在某个分量 $U_j$ 上不是零多项式，进而导致理想 $\bar I$ 的约简Groebner基不是 ${1\}$ ，算法失败。

令 $W$ 是关于坐标 $u_1,\cdots,u_m,x_1,\cdots,x_n$ 的仿射空间 $\mathbb R^{m+n}$ 上的不可约簇，我们说函数 $u_1,\cdots,u_m$ 在 $W$ 上是代数独立的（algebraically independent ），如果任意的仅关于 $u_i$ 的非零多项式在 $W$ ?上不会同时消失（no nonzero polynomial in the $u_i$ alone vanishes identically on $W$ ），即 $\cap \mathbb R[u_1,\cdots,u_m] = \{0\}$

给定一个簇，
$\pmb V(h_1,\cdots,h_n) \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$
做如下的最小分解：
$(W_1 \cup \cdots \cup W_p) \cup (U_1 \cup \cdots \cup U_q)$
在不可约分量 $W_i$ 上自由变量 $u_1,\cdots,u_m$ 是代数独立的，在不可约分量 $U_j$ 上自由变量 $u_1,\cdots,u_m$ 不是代数独立的（退化情况）。我们仅考虑子簇：
$W_1 \cup \cdots \cup W_p \subseteq V$
我们说结论 $g$ 普遍地遵循（follows generically）前提 $h_1,\cdots,h_n$ ，如果 $\in \pmb I(V') \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$ ，其中簇 $V^{'}$ 就是上述分解中的 $\pmb V(h_1,\cdots,h_n)$ 的子簇。

自动化证明

给定一个几何声明的前提 $h_1,\cdots,h_n$ 和结论 $g$ ，为了证明这个声明的正确性，需要使得：结论 $g$ 普遍地遵循前提 $h_1,\cdots,h_n$ ，也就是说 $\in \pmb I(V')$

然而，将一个簇分解为不可约簇并不是很容易。幸运的是，即使不知道最小分解，我们依然可以确定 $g$ 是否属于 $\pmb I(V')$

Proposition：结论 $g$ 普遍地遵循前提 $h_1,\cdots,h_n$ ，如果存在一些仅关于自由变量的非零多项式 $c(u_1,\cdots,u_m) \in \mathbb R[u_1,\cdots,u_m]$ ，使得
$\cdot g \in \sqrt{H}$
这里 $<h_1,\cdots,h_n> \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$

proof：令 $V_j$ 是 $V^{'}$ 的一个不可约分量。由于 $\cdot g \in \sqrt{H}$ ，因此 $\cdot g$ 在簇 $\pmb V(\sqrt{H}) = \pmb V(H) = V$ 上消失，自然也在 $V_j$ 上消失，即 $\cdot g \in \pmb I(V_j)$ 。由于 $V_j$ 是不可约的，因此 $\pmb I(V_j)$ 是素的。同时， $c$ 是仅关于自由变量的非零多项式，根据 $I(V_j) \cap \mathbb R[u_1,\cdots,u_m] = \{0\}$ ，得到 $\notin \pmb I(V_j)$ ，所以一定有 $\in \pmb I(V_j)$ ，推出 $\in \pmb I(V')$

下面，我们给出判断是否存在 $\in \mathbb R[u_1,\cdots,u_m]$ 的算法：

易知， $\cdot g \in \sqrt{H} \iff (c \cdot g)^s = \sum_{j=1}^n A_j h_j$ ，其中 $A_j \in \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$ ， $\ge 1$

两边同除 $c^s$ ，得到
$g^s = \sum_{j=1}^n \dfrac{A_j}{c^s} h_j$
做分式域 $\mathbb R(u_1,\cdots,u_m):= FF(\mathbb R[u_1,\cdots,u_m])$ ，构造理想
$\tilde H = <h_1,\cdots,h_n> \subseteq \mathbb R(u_1,\cdots,u_m)[x_1,\cdots,x_n]$
那么 $\in \sqrt{\tilde H}$ 。易证， $\in \sqrt{\tilde H} \iff c \cdot g \in \sqrt{H}$

自动化证明算法如下：

给定几何命题，确定坐标中的自由变量 $u_1,\cdots,u_m$ 和不自由变量 $x_1,\cdots,x_n$ ，然后翻译为环 $\mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]$ 上的多项式
前提 $h_1,\cdots,h_n$ ，结论 $g$ ，构造理想
$\bar H = <h_1,\cdots,h_n,1-yg> \subseteq \mathbb R(u_1,\cdots,u_m)[x_1,\cdots,x_n,y]$
计算理想 $\bar H$ 的约化Groebner基 $G$ ，那么
$\in \sqrt{\tilde H} \iff \{1\} = G$
如果 $G=\{1\}$ ，那么结论 $g$ 普遍地遵循前提 $h_1,\cdots,h_n$ ，几何定理证明完毕；否则，这个声明是假的。

扩展

进一步的，有如下性质：

可以证明，
$\{1\} = G \iff \bar H \cap \mathbb R[u_1,\cdots,u_m] \neq \{0\}$
如果 $\in \bar H \cap \mathbb R[u_1,\cdots,u_m]$ ，那么 $\cdot g \in \sqrt{H}$ 。再利用 the algorithm for computing intersections of ideals，就可以计算出满足 $\cdot g \in \sqrt H$ 的一些多项式 $\in \mathbb R[u_1,\cdots,u_m]$
如果 $g$ 在某些 $u_1,\cdots,u_m$ 的取值下失败，那么
$(u_1,\cdots,u_m) \in W = \pmb V(\bar H \cap \mathbb R[u_1,\cdots,u_m])$
即簇 $W$ 记录了所有的退化情况。
实际上，
$\cdot g \in \sqrt H \iff c \in \sqrt{\bar H \cap \mathbb R[u_1,\cdots,u_m]}$
即这个根理想记录了 $c$ 的所有可能的取值。