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