中科大数学实验课件15初等几何定理的计算机证明_第1页
中科大数学实验课件15初等几何定理的计算机证明_第2页
中科大数学实验课件15初等几何定理的计算机证明_第3页
中科大数学实验课件15初等几何定理的计算机证明_第4页
中科大数学实验课件15初等几何定理的计算机证明_第5页
已阅读5页，还剩23页未读， 继续免费阅读

下载本文档

版权说明：本文档由用户提供并上传，收益归属内容提供方，若内容存在侵权，请进行举报或认领

文档简介

1、数学实验之十五-初等几何定理的计算机证明主要内容符号计算与自动推理几何问题代数化代数关系式的推导与验证自动推理1、符号计算与自动推理符号计算 精确的、带未知变元的、公式的推导与验证。 符号运算 自动推理自动推理 从已知条件推导出结果，即计算机自动证明定理、或推导出新的未知的结论。 数学定理的机器证明 把一类定理作为一个整体加以考虑，建立一个统一的、确定的证明程序，对该类定理中的每一个定理，应用证明程序进行有限步推理之后即可从命题的假设推出命题的结论。 计算机自动推理实例 计算机象棋、四色定理、初等几何定理 的计算机证明2、几何问题代数化解析几何是基础 笛卡儿名言： 一切问题都可以化为数学问题

2、一切数学问题都可以化为代数问题 一切代数问题都可以化为方程求解 点 坐标线 方程几何图形 方程组几何关系 方程组条件 方程组结论 方程组例 1 证明平行四边形两对角线相互平分 BACDN建立直角坐标系如图。A,B,C的坐标如下其中 为自由参数。再设D,N的坐标为 ， 则 可以由 所表示。 利用条件AB/CD, AC/BD，可得于是利用条件（1），条件（2）可以简化为再由A,N,D共线，B,N,C共线有由此，至此，定理的条件化为（1）-（4）。由AN=ND,BN=NC,定理的结论化为例 2 证明三角形三边上的垂线交于一点。ABCDEFG建立坐标系如图。设由B,D,C共线及AD与BC垂直有因此，同

3、理，由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 对 整除所得的余式： 其中 表示以 为主变元， 被 整除所得到的伪余式。3、如果 ，则在某些条件下，可以从（I） 推导出 (II)。伪除法：给定两个多项式其中 是关于 的多项式，且 。 以 做主变元做多项式除法其中 是有理式，分母都是 的某个次幂（设为 s）。用 同乘上式两边这里 是关于 的多项式。 称为f 被 g 整除的伪余式。例如，对于因此吴方法的实现第一步：消元。通过伪除法实现。例如，从下列方程组中消去第二步：逐次伪除法。从上式得其中 为多项式。如果 ，则在条件下，由 （I）可以推出 （II）。例 1（续）：我们要从方程组(1)(4)推出（5）与（6）。为此，先三角化方程组(1)(4).由此，（5）在条件 下成立。4、自动推理由一些变量之间的已知关系推导一些变量之间的未知关系。例 3 推导正五边形的边长与连接不相邻的两个顶点的线

人人文库> 全部分类> 教育资料 > 课件下载

温馨提示

  • 1. 本站所有资源如无特殊说明，都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等，如果需要附件，请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸，网页内容里面会有图纸预览，若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对用户上传分享的文档内容本身不做任何修改或编辑，并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容，请与我们联系，我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

最新文档

评论

0/150

提交评论