《初等几何定理的计算机证明课件.ppt》由会员分享，可在线阅读，更多相关《初等几何定理的计算机证明课件.ppt（28页珍藏版）》请在三一办公上搜索。
1、数学实验之十五-初等几何定理的计算机证明,中国科学技术大学数学系陈发来,主要内容,符号计算与自动推理几何问题代数化代数关系式的推导与验证自动推理,1、符号计算与自动推理,符号计算 精确的、带未知变元的、公式的推导与验证。符号运算 自动推理自动推理 从已知条件推导出结果，即计算机自动证明定理、或推导出新的未知的结论。,数学定理的机器证明 把一类定理作为一个整体加以考虑，建立一个统一的、确定的证明程序，对该类定理中的每一个定理，应用证明程序进行有限步推理之后即可从命题的假设推出命题的结论。计算机自动推理实例 计算机象棋、四色定理、初等几何定理 的计算机证明,2、几何问题代数化,解析几何是基础 笛卡
2、儿名言：一切问题都可以化为数学问题 一切数学问题都可以化为代数问题 一切代数问题都可以化为方程求解,点 坐标线 方程几何图形 方程组几何关系 方程组条件 方程组结论 方程组,例 1 证明平行四边形两对角线相互平分,B,A,C,D,N,建立直角坐标系如图。A,B,C的坐标如下,其中 为自由参数。再设D,N的坐标为，则 可以由 所表示。利用条件AB/CD,AC/BD，可得,于是,利用条件（1），条件（2）可以简化为,再由A,N,D共线，B,N,C共线有,由此，,至此，定理的条件化为（1）-（4）。由AN=ND,BN=NC,定理的结论化为,例 2 证明三角形三边上的垂线交于一点。,A,B,C,D,E
3、,F,G,建立坐标系如图。设,由B,D,C共线及AD与BC垂直有,因此，,同理，由A,E,C共线及BE与AC垂直有,再由A,G,D与B,G,E分别共线有,结论：,两个问题：1、方程与给定的条件与结论是否等价？2、如何由给定的一组方程推出另外一 组方程成立？下面以例1为例来说明问题1。在条件：下等价。,3、代数关系式的推导与验证,给定多项式方程组：,其中 为参数。如何从上述方程组推导出,思路：寻找函数i=1,n,使得则由（I）可以推出（II）。吴方法可以实现上述过程。,吴方法的步骤：1、将方程组（I）化为三角型方程组：,2、计算 g 对 整除所得的余式：,其中 表示以 为主变元，被 整除所得到的
4、伪余式。3、如果，则在某些条件下，可以从（I）推导出(II)。,伪除法：给定两个多项式,其中 是关于 的多项式，且。以 做主变元做多项式除法其中 是有理式，分母都是 的某个次幂（设为 s）。用 同乘上式两边,这里 是关于 的多项式。称为f 被 g 整除的伪余式。例如，对于,因此,吴方法的实现第一步：消元。通过伪除法实现。例如，从下列方程组中消去,第二步：逐次伪除法。,从上式得其中 为多项式。,如果，则在条件下，由（I）可以推出（II）。例 1（续）：我们要从方程组(1)(4)推出（5）与（6）。为此，先三角化方程组(1)(4).,由此，（5）在条件 下成立。,4、自动推理,由一些变量之间的已知关系推导一些变量之间的未知关系。例 3 推导正五边形的边长与连接不相邻的两个顶点的线段长度之间的关系。,A,B,C,D,E,O,x,y,以正五边形中心为坐标原点建立直角坐标系如图。设 则 由ABCDE为正五边形有,三角化后得,由此,
