数学实验之十五 ---
初等几何定理的计算机证明中国科学技术大学数学系陈发来主要内容
符号计算与自动推理
几何问题代数化
代数关系式的推导与验证
自动推理
1、符号计算与自动推理
符号计算精确的、带未知变元的、公式的推导与验证。
符号运算 自动推理
自动推理从已知条件推导出结果，即计算机自动证明定理、或推导出新的未知的结论。
数学定理的机器证明把一类定理作为一个整体加以考虑，建立一个统一的、确定的证明程序，对该类定理中的每一个定理，应用证明程序进行有限步推理之后即可从命题的假设推出命题的结论。
计算机自动推理实例计算机象棋、四色定理、初等几何定理的计算机证明
2、几何问题代数化
解析几何是基础笛卡儿名言：
一切问题都可以化为数学问题一切数学问题都可以化为代数问题一切代数问题都可以化为方程求解点 坐标线 方程几何图形 方程组几何关系 方程组条件 方程组结论 方程组例 1 证明平行四边形两对角线相互平分
BA
C D
N
建立直角坐标系如图。 A,B,C的坐标如下
),(),0,(),0,0( 321 uuCuBA
其中 为自由参数。再设 D,N的坐标为,则可以由 所表示。
利用条件 AB//CD,AC//BD,可得
321,,uuu
),(),,( 4321 xxNxxD 4321,,,xxxx
321,,uuu
2
3
11
2
21
32
0
u
u
ux
x
ux
ux
于是
)2(0)(:
)1(0:
223112
321
uxuuxh
uxh
利用条件（ 1），条件（ 2）可以简化为
)2(0,'211'2 uuxh
再由 A,N,D共线,B,N,C共线有
1
3
3
4
x
u
x
x?
12
3
13
4
uu
u
ux
x
由此，
)4(0)()(:
)3(0:
3131244
33143
uuxuuxh
uxxxh
至此，定理的条件化为（ 1） --（ 4）。
由 AN=ND,BN=NC,定理的结论化为
)6(02)(2:
)5(022:
2
3
2
2
2
1342132
2
24231
2
11
uuuuxuuxg
xxxxxxg
例 2 证明三角形三边上的垂线交于一点。
A B
C
DE
F
G
建立坐标系如图。设 )0,(),0,(
21 uBuA
),(),,(),,(),,0( 6543213 xxGxxExxDuC
由 B,D,C共线及 AD与 BC垂直有
1
2
3
11
2
2
3
21
2
u
u
ux
x
u
u
ux
x
因此，
)2(0)(:
)1(0)(:
112232
213221
uxuxuh
uxuxuh
同理，由 A,E,C共线及 BE与 AC垂直有
)4(0)(:
)3(0)(:
232434
133413
uxuxuh
uxuxuh
再由 A,G,D与 B,G,E分别共线有
)6(0)()(:
)5(0)()(:
1161526
2362545
uxxuxxh
uxxuxxh
结论：
)7(05?x
两个问题：
1、方程与给定的条件与结论是否等价？
2、如何由给定的一组方程推出另外一组方程成立？
下面以例 1为例来说明问题 1。
在条件,下等价。
031?uu
3、代数关系式的推导与验证给定多项式方程组：
)(
0),.,,,,,.,,,(
...,,,,,,,,,
0),.,,,,,.,,,(
11
111
I
xxuuh
xxuuh
nmn
nm
其中 为参数。如何从上述方程组推导出 m
uu,...,1
)(0),.,,,,,.,,,( 11 IIxxuug nm?
思路：寻找函数
i=1,…,n,使得则由（ I） 可以推出（ II）。
吴方法可以实现上述过程。
,0),...,,,...,( 11?nmi xxuuq
)(.,,,2211 I I Ihqhqhqg nn
吴方法的步骤：
1、将方程组（ I） 化为三角型方程组：
)(
0),.,,,,,.,,,(
...,,,,,,,,,
0),,.,,,(
11
111
IV
xxuuf
xuuf
nmn
m
2、计算 g 对 整除所得的余式：
1,...,ffn
)(
),,(Re
...,,,,,,,,,
),(Re
),,(Re
1110
11,12
1
V
xfRmR
xfRmR
xfgmR
nnnn
nnn
其中 表示以 为主变元，
被 整除所得到的伪余式。
3、如果,则在某些条件下，可以从（ I） 推导出 (II)。
),,(Re iii xfRm ix
iR if
00?R
伪除法：给定两个多项式
01
01
...
...
dydydg
cycycf
n
n
m
m
其中 是关于 的多项式，
且 。 以 做主变元做多项式除法其中 是有理式，分母都是 的某个次幂（设为 s）。 用 同乘上式两边
ii dc,nxx,...,1
mn? y
rgqf ~~
rq ~,~ nd
snd
rqgfd sn
这里 是关于 的多项式。
称为 f 被 g 整除的伪余式。
例如，对于
yxx n,,...,1rq,
),,(Re ygfmr?
2,332 yxgyyxf
62 28),,(Re xxygfm
626252833 28)42()( xxgxxyxyxfx
因此吴方法的实现第一步：消元。通过伪除法实现。
例如，从下列方程组中消去
3
212
2
2
2
11
1 xxh
xxh
2x
22112123 1),,(Re xxxxhhmh
612112314 21),,(Re xxxxhhmh
第二步：逐次伪除法。
)(
...,,,,,,,,,
01111
21111
1
1
1
VI
RfqRd
RfqRd
Rfqgd
s
nnnn
s
n
nnn
s
n
n
n
从上式得其中 为多项式。
)(.....,0111 1 V I IRfAfAgdd nnsns n
nAA,...,1
如果,则在条件下，由 （ I） 可以推出 （ II）。
例 1（续）：我们要从方程组 (1)— (4)推出（ 5）与（ 6）。为此，先三角化方程组 (1)— (4).
00?R
0...21?nddd
322211'21,uxfuuxhf
31333213314433 )(),,(Re xxuxuuxxuuxhhmf
31312444 )()( uuxuuxhf
0)()(:
0)(
0
0
3131244
31333213313
322
2111
uuxuuxf
xxuxuuxxuuf
uxf
uuxf
313312311
2
22
2
12
2
114413
222
),,(Re
xxuxxuxxuxu
xuxuxfgmR
)2
()(),,(Re
2
21
2
22
2
21231
3
1
2
12
2
113213332
xxxuxuxuuxxu
xuuuuxfRmR
))(()(),,(Re 21231213212221 xuxuuuuuxfRmR
0),,(Re 1110 xfRmR
由此，（ 5）在条件下成立。
0,0)( 12421133 uuIuuxuI
4、自动推理
由一些变量之间的已知关系推导一些变量之间的未知关系。
例 3 推导正五边形的边长与连接不相邻的两个顶点的线段长度之间的关系。
A
B
CD
E
O
x
y
以正五边形中心为坐标原点建立直角坐标系如图。设则由 ABCDE为正五边形有
),(),,(),,(),,0( 4242315 xxDxxCxxBxA?
),( 31 xxE? 12 2||,2|| xBExCD
04)(
0)()()(
0
0
2
2
2
53
2
14
2
43
2
12
2
53
2
13
2
5
2
4
2
22
2
5
2
3
2
11
xxxxh
xxxxxxxh
xxxh
xxxh
三角化后得
53
2
3
2
2
2
14
43
2
3
2
221
2
13
2
2
2
2
2
3
2
1
4
2
2
2
2
1
4
12
2
221
2
121
3
21
2242
22422
444
))((4
xxxxxf
xxxxxxxf
xxxxxxxxf
xxxxxxxf
0222121 xxxx
由此
初等几何定理的计算机证明中国科学技术大学数学系陈发来主要内容
符号计算与自动推理
几何问题代数化
代数关系式的推导与验证
自动推理
1、符号计算与自动推理
符号计算精确的、带未知变元的、公式的推导与验证。
符号运算 自动推理
自动推理从已知条件推导出结果，即计算机自动证明定理、或推导出新的未知的结论。
数学定理的机器证明把一类定理作为一个整体加以考虑，建立一个统一的、确定的证明程序，对该类定理中的每一个定理，应用证明程序进行有限步推理之后即可从命题的假设推出命题的结论。
计算机自动推理实例计算机象棋、四色定理、初等几何定理的计算机证明
2、几何问题代数化
解析几何是基础笛卡儿名言：
一切问题都可以化为数学问题一切数学问题都可以化为代数问题一切代数问题都可以化为方程求解点 坐标线 方程几何图形 方程组几何关系 方程组条件 方程组结论 方程组例 1 证明平行四边形两对角线相互平分
BA
C D
N
建立直角坐标系如图。 A,B,C的坐标如下
),(),0,(),0,0( 321 uuCuBA
其中 为自由参数。再设 D,N的坐标为,则可以由 所表示。
利用条件 AB//CD,AC//BD,可得
321,,uuu
),(),,( 4321 xxNxxD 4321,,,xxxx
321,,uuu
2
3
11
2
21
32
0
u
u
ux
x
ux
ux
于是
)2(0)(:
)1(0:
223112
321
uxuuxh
uxh
利用条件（ 1），条件（ 2）可以简化为
)2(0,'211'2 uuxh
再由 A,N,D共线,B,N,C共线有
1
3
3
4
x
u
x
x?
12
3
13
4
uu
u
ux
x
由此，
)4(0)()(:
)3(0:
3131244
33143
uuxuuxh
uxxxh
至此，定理的条件化为（ 1） --（ 4）。
由 AN=ND,BN=NC,定理的结论化为
)6(02)(2:
)5(022:
2
3
2
2
2
1342132
2
24231
2
11
uuuuxuuxg
xxxxxxg
例 2 证明三角形三边上的垂线交于一点。
A B
C
DE
F
G
建立坐标系如图。设 )0,(),0,(
21 uBuA
),(),,(),,(),,0( 6543213 xxGxxExxDuC
由 B,D,C共线及 AD与 BC垂直有
1
2
3
11
2
2
3
21
2
u
u
ux
x
u
u
ux
x
因此，
)2(0)(:
)1(0)(:
112232
213221
uxuxuh
uxuxuh
同理，由 A,E,C共线及 BE与 AC垂直有
)4(0)(:
)3(0)(:
232434
133413
uxuxuh
uxuxuh
再由 A,G,D与 B,G,E分别共线有
)6(0)()(:
)5(0)()(:
1161526
2362545
uxxuxxh
uxxuxxh
结论：
)7(05?x
两个问题：
1、方程与给定的条件与结论是否等价？
2、如何由给定的一组方程推出另外一组方程成立？
下面以例 1为例来说明问题 1。
在条件,下等价。
031?uu
3、代数关系式的推导与验证给定多项式方程组：
)(
0),.,,,,,.,,,(
...,,,,,,,,,
0),.,,,,,.,,,(
11
111
I
xxuuh
xxuuh
nmn
nm
其中 为参数。如何从上述方程组推导出 m
uu,...,1
)(0),.,,,,,.,,,( 11 IIxxuug nm?
思路：寻找函数
i=1,…,n,使得则由（ I） 可以推出（ II）。
吴方法可以实现上述过程。
,0),...,,,...,( 11?nmi xxuuq
)(.,,,2211 I I Ihqhqhqg nn
吴方法的步骤：
1、将方程组（ I） 化为三角型方程组：
)(
0),.,,,,,.,,,(
...,,,,,,,,,
0),,.,,,(
11
111
IV
xxuuf
xuuf
nmn
m
2、计算 g 对 整除所得的余式：
1,...,ffn
)(
),,(Re
...,,,,,,,,,
),(Re
),,(Re
1110
11,12
1
V
xfRmR
xfRmR
xfgmR
nnnn
nnn
其中 表示以 为主变元，
被 整除所得到的伪余式。
3、如果,则在某些条件下，可以从（ I） 推导出 (II)。
),,(Re iii xfRm ix
iR if
00?R
伪除法：给定两个多项式
01
01
...
...
dydydg
cycycf
n
n
m
m
其中 是关于 的多项式，
且 。 以 做主变元做多项式除法其中 是有理式，分母都是 的某个次幂（设为 s）。 用 同乘上式两边
ii dc,nxx,...,1
mn? y
rgqf ~~
rq ~,~ nd
snd
rqgfd sn
这里 是关于 的多项式。
称为 f 被 g 整除的伪余式。
例如，对于
yxx n,,...,1rq,
),,(Re ygfmr?
2,332 yxgyyxf
62 28),,(Re xxygfm
626252833 28)42()( xxgxxyxyxfx
因此吴方法的实现第一步：消元。通过伪除法实现。
例如，从下列方程组中消去
3
212
2
2
2
11
1 xxh
xxh
2x
22112123 1),,(Re xxxxhhmh
612112314 21),,(Re xxxxhhmh
第二步：逐次伪除法。
)(
...,,,,,,,,,
01111
21111
1
1
1
VI
RfqRd
RfqRd
Rfqgd
s
nnnn
s
n
nnn
s
n
n
n
从上式得其中 为多项式。
)(.....,0111 1 V I IRfAfAgdd nnsns n
nAA,...,1
如果,则在条件下，由 （ I） 可以推出 （ II）。
例 1（续）：我们要从方程组 (1)— (4)推出（ 5）与（ 6）。为此，先三角化方程组 (1)— (4).
00?R
0...21?nddd
322211'21,uxfuuxhf
31333213314433 )(),,(Re xxuxuuxxuuxhhmf
31312444 )()( uuxuuxhf
0)()(:
0)(
0
0
3131244
31333213313
322
2111
uuxuuxf
xxuxuuxxuuf
uxf
uuxf
313312311
2
22
2
12
2
114413
222
),,(Re
xxuxxuxxuxu
xuxuxfgmR
)2
()(),,(Re
2
21
2
22
2
21231
3
1
2
12
2
113213332
xxxuxuxuuxxu
xuuuuxfRmR
))(()(),,(Re 21231213212221 xuxuuuuuxfRmR
0),,(Re 1110 xfRmR
由此，（ 5）在条件下成立。
0,0)( 12421133 uuIuuxuI
4、自动推理
由一些变量之间的已知关系推导一些变量之间的未知关系。
例 3 推导正五边形的边长与连接不相邻的两个顶点的线段长度之间的关系。
A
B
CD
E
O
x
y
以正五边形中心为坐标原点建立直角坐标系如图。设则由 ABCDE为正五边形有
),(),,(),,(),,0( 4242315 xxDxxCxxBxA?
),( 31 xxE? 12 2||,2|| xBExCD
04)(
0)()()(
0
0
2
2
2
53
2
14
2
43
2
12
2
53
2
13
2
5
2
4
2
22
2
5
2
3
2
11
xxxxh
xxxxxxxh
xxxh
xxxh
三角化后得
53
2
3
2
2
2
14
43
2
3
2
221
2
13
2
2
2
2
2
3
2
1
4
2
2
2
2
1
4
12
2
221
2
121
3
21
2242
22422
444
))((4
xxxxxf
xxxxxxxf
xxxxxxxxf
xxxxxxxf
0222121 xxxx
由此
