思路
对于几何定理(geometric theorems)的证明,可以通过引入笛卡尔坐标系,然后将前提(hypotheses)和结论(conclusions)描述为关于命题中点的坐标的多项式方程。令 A , B , C , D , E , F A,B,C,D,E,F A,B,C,D,E,F都是实数空间中的点,
- 线段平行, A B ‾ ∥ C D ‾ \overline{AB} \| \overline{CD} AB∥CD
- 线段垂直, A B ‾ ⊥ C D ‾ \overline{AB} \perp \overline{CD} AB⊥CD
- A , B , C A,B,C A,B,C三点共线(collinear)
- 距离相等, A B = C D AB=CD AB=CD
- C C C落在以 A A A为中心 A B AB AB为半径的圆上
- C C C是 A B ‾ \overline{AB} AB的中点
- 锐角相等, ∠ A B C = ∠ D E F \angle ABC = \angle DEF ∠ABC=∠DEF
- B D ‾ \overline{BD} BD平分角 ∠ A B C \angle ABC ∠ABC
- ⋯ \cdots ⋯
这些基本的几何性质,都可以用关于点坐标的多项式来描述。
我们说一个几何定理是可接受的(admissible),如果它的前提和结论都可以被翻译为多项式方程。
给定任意一个几何定理,总有一些点的坐标是任意的(arbitrary),也总有另一些点的坐标是确定的(determined)。定义自变量(independent variables)为
u
1
,
⋯
,
u
m
u_1,\cdots,u_m
u1,⋯,um,定义因变量(dependent variables)为
x
1
,
…
,
x
n
x_1,\dots,x_n
x1,…,xn,那么可接受的几何定理的前提可以描述为一组多项式
h
1
(
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
)
=
0
,
h
2
(
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
)
=
0
,
⋮
h
n
(
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
)
=
0.
\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}
h1(u1,⋯,um,x1,⋯,xn)h2(u1,⋯,um,x1,⋯,xn)⋮hn(u1,⋯,um,x1,⋯,xn)=0,=0,=0.
同时,可接受的几何定理的结论可以描述为单个多项式(如果结论包含了一组多项式,也依旧可以一个个地解决)
g
(
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
)
=
0.
g(u_1,\cdots,u_m,x_1,\cdots,x_n) = 0.
g(u1,⋯,um,x1,⋯,xn)=0.
严格遵循
我们说结论 g g g严格地遵循(follows strictly)前提 h 1 , ⋯ , h n h_1,\cdots,h_n h1,⋯,hn,如果 g ∈ I ( V ) ⊆ R [ u 1 , ⋯ , u m , x 1 , ⋯ , x n ] g \in \pmb I(V) \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n] g∈III(V)⊆R[u1,⋯,um,x1,⋯,xn],其中簇 V = V ( h 1 , ⋯ , h n ) V = \pmb V(h_1,\cdots,h_n) V=VVV(h1,⋯,hn)
充分不必要条件:如果
g
∈
<
h
1
,
⋯
,
h
n
>
g \in \sqrt{<h_1,\cdots,h_n>}
g∈<h1,⋯,hn>
利用 the radical membership algorithm,定义理想
I
ˉ
=
<
h
1
,
⋯
,
h
n
,
1
−
y
g
>
⊆
R
[
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
,
y
]
\bar I = <h_1,\cdots,h_n,1-yg> \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n,y]
Iˉ=<h1,⋯,hn,1−yg>⊆R[u1,⋯,um,x1,⋯,xn,y]
那么
g
∈
<
h
1
,
⋯
,
h
n
>
⟺
G
=
{
1
}
g \in \sqrt{<h_1,\cdots,h_n>} \iff G = \{1\}
g∈<h1,⋯,hn>
仅当
<
h
1
,
⋯
,
h
n
>
=
I
(
V
)
\sqrt{<h_1,\cdots,h_n>} = \pmb I(V)
<h1,⋯,hn>
普遍遵循
然而,上述的严格遵循
过于严格,没有考虑“退化”情况(degenerate cases):令
V
=
V
(
h
1
,
⋯
,
h
n
)
V = \pmb V(h_1,\cdots,h_n)
V=VVV(h1,⋯,hn),做簇的最小分解
V
=
U
1
∪
⋯
∪
U
s
V = U_1 \cup \cdots \cup U_s
V=U1∪⋯∪Us,某个自由变量
u
i
u_i
ui在某个簇
U
j
U_j
Uj上不再自由。例如,
U
2
=
V
(
x
1
,
x
2
−
u
3
,
u
1
)
U_2 = \pmb V(x_1,x_2-u_3,u_1)
U2=VVV(x1,x2−u3,u1),那么
u
1
=
0
u_1 = 0
u1=0不再能够任意取值。这种退化会使得
g
g
g在某个分量
U
j
U_j
Uj上不是零多项式,进而导致理想
I
ˉ
\bar I
Iˉ的约简Groebner基不是
{
1
}
\{1\}
{1},算法失败。
令 W W W是关于坐标 u 1 , ⋯ , u m , x 1 , ⋯ , x n u_1,\cdots,u_m,x_1,\cdots,x_n u1,⋯,um,x1,⋯,xn的仿射空间 R m + n \mathbb R^{m+n} Rm+n上的不可约簇,我们说函数 u 1 , ⋯ , u m u_1,\cdots,u_m u1,⋯,um在 W W W上是代数独立的(algebraically independent ),如果任意的仅关于 u i u_i ui的非零多项式在 W W W上不会同时消失(no nonzero polynomial in the u i u_i ui alone vanishes identically on W W W),即 I ( W ) ∩ R [ u 1 , ⋯ , u m ] = { 0 } I(W) \cap \mathbb R[u_1,\cdots,u_m] = \{0\} I(W)∩R[u1,⋯,um]={0}
给定一个簇,
V
=
V
(
h
1
,
⋯
,
h
n
)
⊆
R
[
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
]
V = \pmb V(h_1,\cdots,h_n) \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]
V=VVV(h1,⋯,hn)⊆R[u1,⋯,um,x1,⋯,xn]
做如下的最小分解:
V
=
(
W
1
∪
⋯
∪
W
p
)
∪
(
U
1
∪
⋯
∪
U
q
)
V = (W_1 \cup \cdots \cup W_p) \cup (U_1 \cup \cdots \cup U_q)
V=(W1∪⋯∪Wp)∪(U1∪⋯∪Uq)
在不可约分量
W
i
W_i
Wi上自由变量
u
1
,
⋯
,
u
m
u_1,\cdots,u_m
u1,⋯,um是代数独立的,在不可约分量
U
j
U_j
Uj上自由变量
u
1
,
⋯
,
u
m
u_1,\cdots,u_m
u1,⋯,um不是代数独立的(退化情况)。我们仅考虑子簇:
V
′
=
W
1
∪
⋯
∪
W
p
⊆
V
V' = W_1 \cup \cdots \cup W_p \subseteq V
V′=W1∪⋯∪Wp⊆V
我们说结论
g
g
g普遍地遵循(follows generically)前提
h
1
,
⋯
,
h
n
h_1,\cdots,h_n
h1,⋯,hn,如果
g
∈
I
(
V
′
)
⊆
R
[
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
]
g \in \pmb I(V') \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]
g∈III(V′)⊆R[u1,⋯,um,x1,⋯,xn],其中簇
V
′
V'
V′就是上述分解中的
V
(
h
1
,
⋯
,
h
n
)
\pmb V(h_1,\cdots,h_n)
VVV(h1,⋯,hn)的子簇。
自动化证明
给定一个几何声明的前提 h 1 , ⋯ , h n h_1,\cdots,h_n h1,⋯,hn和结论 g g g,为了证明这个声明的正确性,需要使得:结论 g g g普遍地遵循前提 h 1 , ⋯ , h n h_1,\cdots,h_n h1,⋯,hn,也就是说 g ∈ I ( V ′ ) g \in \pmb I(V') g∈III(V′)
然而,将一个簇分解为不可约簇并不是很容易。幸运的是,即使不知道最小分解,我们依然可以确定 g g g是否属于 I ( V ′ ) \pmb I(V') III(V′)
Proposition:结论
g
g
g普遍地遵循前提
h
1
,
⋯
,
h
n
h_1,\cdots,h_n
h1,⋯,hn,如果存在一些仅关于自由变量的非零多项式
c
(
u
1
,
⋯
,
u
m
)
∈
R
[
u
1
,
⋯
,
u
m
]
c(u_1,\cdots,u_m) \in \mathbb R[u_1,\cdots,u_m]
c(u1,⋯,um)∈R[u1,⋯,um],使得
c
⋅
g
∈
H
c \cdot g \in \sqrt{H}
c⋅g∈H
这里
H
=
<
h
1
,
⋯
,
h
n
>
⊆
R
[
u
1
,
⋯
,
u
m
,
x
1
,
⋯
,
x
n
]
H = <h_1,\cdots,h_n> \subseteq \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n]
H=<h1,⋯,hn>⊆R[u1,⋯,um,x1,⋯,xn]
proof:令
V
j
V_j
Vj是
V
′
V'
V′的一个不可约分量。由于
c
⋅
g
∈
H
c \cdot g \in \sqrt{H}
c⋅g∈H
下面,我们给出判断是否存在 c ∈ R [ u 1 , ⋯ , u m ] c \in \mathbb R[u_1,\cdots,u_m] c∈R[u1,⋯,um]的算法:
易知,
c
⋅
g
∈
H
⟺
(
c
⋅
g
)
s
=
∑
j
=
1
n
A
j
h
j
c \cdot g \in \sqrt{H} \iff (c \cdot g)^s = \sum_{j=1}^n A_j h_j
c⋅g∈H
两边同除
c
s
c^s
cs,得到
g
s
=
∑
j
=
1
n
A
j
c
s
h
j
g^s = \sum_{j=1}^n \dfrac{A_j}{c^s} h_j
gs=j=1∑ncsAjhj
做分式域
R
(
u
1
,
⋯
,
u
m
)
:
=
F
F
(
R
[
u
1
,
⋯
,
u
m
]
)
\mathbb R(u_1,\cdots,u_m):= FF(\mathbb R[u_1,\cdots,u_m])
R(u1,⋯,um):=FF(R[u1,⋯,um]),构造理想
H
~
=
<
h
1
,
⋯
,
h
n
>
⊆
R
(
u
1
,
⋯
,
u
m
)
[
x
1
,
⋯
,
x
n
]
\tilde H = <h_1,\cdots,h_n> \subseteq \mathbb R(u_1,\cdots,u_m)[x_1,\cdots,x_n]
H~=<h1,⋯,hn>⊆R(u1,⋯,um)[x1,⋯,xn]
那么
g
∈
H
~
g \in \sqrt{\tilde H}
g∈H~
自动化证明算法如下:
-
给定几何命题,确定坐标中的自由变量 u 1 , ⋯ , u m u_1,\cdots,u_m u1,⋯,um和不自由变量 x 1 , ⋯ , x n x_1,\cdots,x_n x1,⋯,xn,然后翻译为环 R [ u 1 , ⋯ , u m , x 1 , ⋯ , x n ] \mathbb R[u_1,\cdots,u_m,x_1,\cdots,x_n] R[u1,⋯,um,x1,⋯,xn]上的多项式
-
前提 h 1 , ⋯ , h n h_1,\cdots,h_n h1,⋯,hn,结论 g g g,构造理想
H ˉ = < h 1 , ⋯ , h n , 1 − y g > ⊆ R ( u 1 , ⋯ , u m ) [ x 1 , ⋯ , x n , y ] \bar H = <h_1,\cdots,h_n,1-yg> \subseteq \mathbb R(u_1,\cdots,u_m)[x_1,\cdots,x_n,y] Hˉ=<h1,⋯,hn,1−yg>⊆R(u1,⋯,um)[x1,⋯,xn,y] -
计算理想 H ˉ \bar H Hˉ的约化Groebner基 G G G,那么
g ∈ H ~ ⟺ { 1 } = G g \in \sqrt{\tilde H} \iff \{1\} = G g∈H~⟺{1}=G -
如果 G = { 1 } G=\{1\} G={1},那么结论 g g g普遍地遵循前提 h 1 , ⋯ , h n h_1,\cdots,h_n h1,⋯,hn,几何定理证明完毕;否则,这个声明是假的。
扩展
进一步的,有如下性质:
-
可以证明,
{ 1 } = G ⟺ H ˉ ∩ R [ u 1 , ⋯ , u m ] ≠ { 0 } \{1\} = G \iff \bar H \cap \mathbb R[u_1,\cdots,u_m] \neq \{0\} {1}=G⟺Hˉ∩R[u1,⋯,um]={0} -
如果 c ∈ H ˉ ∩ R [ u 1 , ⋯ , u m ] c \in \bar H \cap \mathbb R[u_1,\cdots,u_m] c∈Hˉ∩R[u1,⋯,um],那么 c ⋅ g ∈ H c \cdot g \in \sqrt{H} c⋅g∈H
。再利用 the algorithm for computing intersections of ideals,就可以计算出满足 c ⋅ g ∈ H c \cdot g \in \sqrt H c⋅g∈H 的一些多项式 c ∈ R [ u 1 , ⋯ , u m ] c \in \mathbb R[u_1,\cdots,u_m] c∈R[u1,⋯,um] -
如果 g g g在某些 u 1 , ⋯ , u m u_1,\cdots,u_m u1,⋯,um的取值下失败,那么
( u 1 , ⋯ , u m ) ∈ W = V ( H ˉ ∩ R [ u 1 , ⋯ , u m ] ) (u_1,\cdots,u_m) \in W = \pmb V(\bar H \cap \mathbb R[u_1,\cdots,u_m]) (u1,⋯,um)∈W=VVV(Hˉ∩R[u1,⋯,um])
即簇 W W W记录了所有的退化情况。 -
实际上,
c ⋅ g ∈ H ⟺ c ∈ H ˉ ∩ R [ u 1 , ⋯ , u m ] c \cdot g \in \sqrt H \iff c \in \sqrt{\bar H \cap \mathbb R[u_1,\cdots,u_m]} c⋅g∈H⟺c∈Hˉ∩R[u1,⋯,um]
即这个根理想记录了 c c c的所有可能的取值。
除了上述介绍的利用Groebner基技术来自动化证明几何定理,还有中科院院士吴文俊的吴方法,提出的更早。它在实际中的表现往往比Groebner基更有效,因此也更常用。这里不再详细介绍。
更多推荐
几何定理的自动化证明(Automatic Geometric Theorem Proving)
发布评论