初等几何定理的计算机证明——科技大学. ppt
数学实验之十五15----初等几何定理的计算机证明我国科技大学数学系lldxh主要内容符号计算和自动推理几何问题代数化代数关系式的推导和验证自动推理1、符号计算和自动推理符号计算精确、具有未知自变量的公式推导和验证。 符号运算自动推理自动推理从已知条件导出结果，即计算机自动证明定理或导出新的未知结论。 2、几何问题代数化解析几何是底层笛卡尔的名言。 所有问题都可以数学问题所有数学问题所有代数问题所有代数问题都可以制成方程来求解。 3、代数关系式的推导和给定多项式方程的验证。 4、自动推理从几个变量之间的已知关系导出几个变量之间的未知关系。 例3导出正五边形的边的长度和连接不相邻的两个顶点的线段的长度的关系。 *数学定理的机械证明，是把一类定理作为整体来考虑，编制统一确定的证明程序，对这类定理分别应用证明程序进行有限步骤推理后，可以从命题的假说中得出命题的结论。 计算机自动推理实例计算机象棋、四色定理、初等几何定理的计算机证明点坐标标线方程几何图形方程组几何关系方程组的条件方程组结论方程组例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 F G坐标系图。 假设b、d、c共线和AD与BC垂直。 因此类似地，可以得出a、e、c共享线和BE与AC垂直，并且a、g、d和b、g、e分别是共享线。 1、方程给出的条件和结论等价吗？ 2、如何从给定的方程中推出另一个方程成立？ 以例1为例来说明问题1吧。 条件：下等效。 这里是参数。 如何从上述方程式中导出想法：查找函数i=1，…，n，使其能够从I )中得出II )。 dcdnht可以实现上述工艺。 dcdnht步骤： 1、方程组()为三角方程) 2、计算除g对得到的馀数公式)其中取主自变量，表示除得到的伪馀数公式。 3、如果是，在一定条件下，可以推导(I )至(II )。 伪除法：给定的两个多项式中关于的多项式，并且。 如果用主变量进行多项式除法，其中有有理式，分母是所有的幂(假设为s )。 上式两边乘方这里是关于的多项式。 被称为伪剩余公式，其中f可以被g整除。 例如，因此实现dcdnht的第一步：消元。 通过模拟除法实现。 例如，从以下方程中删除步骤2 : 是逐次伪除法。 由上式得到多项式。 如果是这样，在条件下，可以推出(I )至(II )。 例1 (续)方程(1) )至(5)和(6)。 因此，先根据三角化方程式(1) )，)5)在条件下成立。 ***