数学实验之十五 初等几何定理的计算机证明 中国科学技术大学数学系 陈发来
数学实验之十五--- 初等几何定理的计算机证明 中国科学技术大学数学系 陈发来
主要内容 符号计算与自动推理 几何问题代数化 代数关系式的推导与验证 自动推理
主要内容 • 符号计算与自动推理 • 几何问题代数化 • 代数关系式的推导与验证 • 自动推理
1、符号计算与自动推理 符号计算 精确的、带未知变元的、公式的推导与 F验证 符号运算 自动推理 自动推理 从已知条件推导出结果,即计算机自动 证明定理、或推导出新的未知的结论
1、符号计算与自动推理 • 符号计算 精确的、带未知变元的、公式的推导与 验证。 符号运算 自动推理 • 自动推理 从已知条件推导出结果，即计算机自动 证明定理、或推导出新的未知的结论
数学定理的机器证明 把一类定理作为一个整体加以考虑,建 立一个统一的、确定的证明程序,对该类 定理中的每一个定理,应用证明程序进行 有限步推理之后即可从命题的假设推出命 题的结论。 计算机自动推理实例 计算机象棋、四色定理、初等几何定理 的计算机证明
• 数学定理的机器证明 把一类定理作为一个整体加以考虑，建 立一个统一的、确定的证明程序，对该类 定理中的每一个定理，应用证明程序进行 有限步推理之后即可从命题的假设推出命 题的结论。 • 计算机自动推理实例 计算机象棋、四色定理、初等几何定理 的计算机证明
2、几何问题代数化 解析几何是基础 笛卡儿名言 切问题都可以化为数学问题 切数学问题都可以化为代数问题 切代数问题都可以化为方程求解
2、几何问题代数化 • 解析几何是基础 笛卡儿名言： 一切问题都可以化为数学问题 一切数学问题都可以化为代数问题 一切代数问题都可以化为方程求解
点线 坐标 方程 几何图形=方程组 几何关系 方程组 条件 方程组 结论 方程组
点 坐标 线 方程 几何图形 方程组 几何关系 方程组 条件 方程组 结论 方程组
例1证明平行四边形两对角线相互平分 建立直角坐标系如图。ABC的坐标如下 A(0,0),B(1,O),C(u2,3)
例 1 证明平行四边形两对角线相互平分 A B C D N 建立直角坐标系如图。A,B,C的坐标如下 (0,0), ( ,0), ( , ) A B u1 C u2 u3
其中l1,2,3为自由参数。再设DN的 坐标为D(x,x2),N(x2,x),则x1,x2x,x4 可以由12u23所表示。 利用条件ABCD,ACBD,可得 x2-l3 于是
其中 为自由参数。再设D,N的 坐标为 ， 则 可以由 所表示。 利用条件AB//CD, AC//BD，可得 1 2 3 u ,u ,u ( , ), ( , ) 1 2 3 4 D x x N x x 1 2 3 4 x , x , x , x 1 2 3 u ,u ,u 2 3 1 1 2 1 2 2 3 0 u u x u x x u x u = − = − − 于是
0 0(2) 利用条件(1),条件(2)可以简 化为 x1-1 0 (2) 再由AND共线,BN,C共线有 X4
: ( ) 0 (2) : 0 (1) 2 1 1 3 2 2 1 2 3 = − − = = − = h x u u x u h x u 利用条件（1），条件（2）可以简 化为 : 0 (2 ) ' 1 1 2 ' h2 = x −u −u = 再由A,N,D共线，B,N,C共线有 1 3 3 4 x u x x =
由此 h3:=x4 0 (3) h2:=x4(l2-41)-(x3-1)2=0(4 至此,定理的条件化为(1)--(4)。 由AN=ND,BN=NC定理的结论化为 81:=x-2x1x3-2x2x4+x2=0 (5) g2=2x3(l1-l2)-2xl2-12+2+2=0(6
2 1 3 3 1 4 u u u x u x − = − 由此， : ( ) ( ) 0 (4) : 0 (3) 4 4 2 1 3 1 3 3 4 1 3 3 = − − − = = − = h x u u x u u h x x x u 至此，定理的条件化为（1）--（4）。 由AN=ND,BN=NC,定理的结论化为 : 2 ( ) 2 0 (6) : 2 2 0 (5) 2 3 2 2 2 2 3 1 2 4 3 1 2 1 3 2 4 2 2 1 1 = − − − + + = = − − + = g x u u x u u u u g x x x x x x