坐标法与机器证明.ppt

坐标法与机器证明阅读与思考阅读与思考三门第二高级中学三门第二高级中学陈雪蛟陈雪蛟笛卡尔的设想笛卡尔的设想一切问题化为数学问题，一切问题化为数学问题，一切数学问题化为代数问题，一切数学问题化为代数问题，一切代数问题化为代数方程一切代数问题化为代数方程求解问题。求解问题。笛卡尔笛卡尔解析几何之父解析几何之父几何问题几何问题的求解或的求解或求证问题求证问题坐标转化坐标转化空间形式的空间形式的推理问题推理问题笛卡尔创立坐标系笛卡尔创立坐标系代数方程的代数方程的求解问题求解问题计算问题计算问题意味着几何定理意味着几何定理机械化证明机械化证明成为了一种成为了一种可能可能。数学机械化数学机械化数学问题的机械化数学问题的机械化-在运算或证明在运算或证明的过程中，每前进一步之后，都有一的过程中，每前进一步之后，都有一个确定的，必须选择的下一步，这样个确定的，必须选择的下一步，这样沿着一条有规律、刻板的道路，一直沿着一条有规律、刻板的道路，一直到达结论。到达结论。数学机械化：从设想到实现数学机械化：从设想到实现他他明确的提出机器可以成为推理工具的思想明确的提出机器可以成为推理工具的思想，由，由于当时的条件限制，计算仅仅是手工操作（手摇于当时的条件限制，计算仅仅是手工操作（手摇计算机），无法进行大量复杂的计算，所以用机计算机），无法进行大量复杂的计算，所以用机器实现几何定理证明的想法无法实现。器实现几何定理证明的想法无法实现。莱莱布布尼尼兹兹吴吴文文俊俊数学机械化：从设想到实现数学机械化：从设想到实现几何定理机器证明几何定理机器证明-“吴方法吴方法”他将几何定理证明从一个不太成功的领域，他将几何定理证明从一个不太成功的领域，变为一个最成功的领域。变为一个最成功的领域。*吴文俊机器证明的思想吴文俊机器证明的思想 吴文俊机器证明的思想吴文俊机器证明的思想主要是从主要是从笛卡尔的坐标法和中国古代解方程的笛卡尔的坐标法和中国古代解方程的计算方法而来，把空间形式的推理转计算方法而来，把空间形式的推理转化成数量关系来处理。化成数量关系来处理。“吴方法吴方法”证明几何定理是基证明几何定理是基于什么样的原理去实现的呢？于什么样的原理去实现的呢？例例 证明：菱形的对角线互相垂直。证明：菱形的对角线互相垂直。几何画板几何画板几何问题代数化几何问题代数化-选取合适坐标选取合适坐标第一步：将已知条件和结论代数化第一步：将已知条件和结论代数化条件条件代数化代数化结论结论代数化代数化第二步：将已知条件多项式整序（三角化）第二步：将已知条件多项式整序（三角化）吴方法的处理吴方法的处理条件多项式整理条件多项式整理目标多项式目标多项式分析：分析：“吴吴方方法法”原原理理第三步：做逐步除法第三步：做逐步除法第一步：将几何定理条件代数化第一步：将几何定理条件代数化定理的结论代数化：定理的结论代数化：“吴方法吴方法”证明几何基本定理的一般步骤证明几何基本定理的一般步骤第二步，将条件方程组整序第二步，将条件方程组整序(消元消元)第二步：将条件多项式整序（三角化）第二步：将条件多项式整序（三角化）第三步：做逐步除法第三步：做逐步除法上述步骤在上述步骤在MathematicaMathematica软件中可以自动完成软件中可以自动完成展望数学机械化的未来展望数学机械化的未来 运用机械化思想考察数学，将会发现数运用机械化思想考察数学，将会发现数学的不同侧面，建立新的模式，活跃和启学的不同侧面，建立新的模式，活跃和启迪思维。机械化数学和数学机械化必将为迪思维。机械化数学和数学机械化必将为数学以致整个科学注入新的活力。数学以致整个科学注入新的活力。