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