数学定理证明机械化的中国学派(II)
2015-07-05 02:19
309 查看
所谓“学派”是指:存在一帮人,具有相同或接近的学术观点或学术立场,采用某种特定的“方法”(或途径),在一个学术方向上共同开展工作,并且做出了相当有迎影响的学术成就。
数学定理证明机械化的途径很多,但是,“吴方法”只有一种。什么是“吴方法”?我们拿初等(平面)几何学为例,所谓“吴方法”实质上就是“方程联立求证法”。什么叫“方程联立求证法”呢?
比如说,我们需要求证一个几何“事实”(或断语):三线“共点”。大家知道,初等平面几何里面有几百条“定理”需要证明,比如,三条直线“共点”,看起来这是显而易见的事情,但是,使用计算机自动证明这一事实却并不容易。
吴方法的第一步:实现“代数化”,即建立坐标系,把问题条件全部翻译成“代数方程式”(事项即“前提条件”),然后,把需要证明的事实也翻译成“代数方程式”(有待证明的事项)。吴方法的第二步:方程联立求证。
把前提条件(方承租)与待证明的方程“联立求解”,如果待证明的“方程”经过自动联立求解过程,变为一个恒等式,那么,这个恒等式就表示“所有前提条件”满足待证的“结论”,所以,定理得到证明,否则,问题无解。
在国际学术界,“吴方法”独树一帜,不随大流,效率最高,得到国际同仁赞扬与肯定。经过多年人才积累,在数学定理证明机械化研究领域,研究业绩非凡,国内”吴氏学派“最终形成。请见:中科院数学机械化国家重点实验室官网。
袁萌 7月5日
数学定理证明机械化的途径很多,但是,“吴方法”只有一种。什么是“吴方法”?我们拿初等(平面)几何学为例,所谓“吴方法”实质上就是“方程联立求证法”。什么叫“方程联立求证法”呢?
比如说,我们需要求证一个几何“事实”(或断语):三线“共点”。大家知道,初等平面几何里面有几百条“定理”需要证明,比如,三条直线“共点”,看起来这是显而易见的事情,但是,使用计算机自动证明这一事实却并不容易。
吴方法的第一步:实现“代数化”,即建立坐标系,把问题条件全部翻译成“代数方程式”(事项即“前提条件”),然后,把需要证明的事实也翻译成“代数方程式”(有待证明的事项)。吴方法的第二步:方程联立求证。
把前提条件(方承租)与待证明的方程“联立求解”,如果待证明的“方程”经过自动联立求解过程,变为一个恒等式,那么,这个恒等式就表示“所有前提条件”满足待证的“结论”,所以,定理得到证明,否则,问题无解。
在国际学术界,“吴方法”独树一帜,不随大流,效率最高,得到国际同仁赞扬与肯定。经过多年人才积累,在数学定理证明机械化研究领域,研究业绩非凡,国内”吴氏学派“最终形成。请见:中科院数学机械化国家重点实验室官网。
袁萌 7月5日
相关文章推荐
- 【网络互联技术】(二) 网络安全的几种解决途径
- 【网络互联技术】(二) 网络安全的几种解决途径
- Maven学习笔记一:安装和基本配置
- java冒泡排序
- Matlab应用实例(1)—fminbnd
- Hadoop Spark 集群简便安装总结
- 【网络互联技术】(一)移动数据加密和网络安全概述
- 【网络互联技术】(一)移动数据加密和网络安全概述
- 理解Linux系统中的load average
- Java多线程—Executor框架
- 摘录-IT企业必读的200个.NET面试题-07 .NET多线程编程
- 我和程序猿的故事2
- fibo数求法(递归版本) -- 作者小泽
- SSH通过密钥登录的设置方法
- 用Eclipse插件Bytecode Outline来查看Java字节码
- 跟着马士兵的视频写的Tankwar 源代码 还有好多需要改进的地方
- hdu 5277 YJC counts stars 暴力
- 求余数
- 254 shades of grey
- QT中遇到的一些问题