博客
关于我
强烈建议你试试无所不能的chatGPT,快点击我
数学定理证明机械化的中国学派(II)
阅读量:5148 次
发布时间:2019-06-13

本文共 653 字,大约阅读时间需要 2 分钟。

 所谓“学派”是指:存在一帮人,具有同样或接近的学术观点或学术立场,採用某种特定的“方法”(或途径),在一个学术方向上共同开展工作。而且做出了相当有迎影响的学术成就。

数学定理证明机械化的途径非常多,可是。“吴方法”仅仅有一种。什么是“吴方法”?我们拿初等(平面)几何学为例,所谓“吴方法”实质上就是“方程联立求证法”。

什么叫“方程联立求证法”呢?

比方说,我们须要求证一个几何“事实”(或断语):三线“共点”。大家知道,初等平面几何里面有几百条“定理”须要证明。比方,三条直线“共点”,看起来这是显而易见的事情。可是,使用计算机自己主动证明这一事实却并不easy。

吴方法的第一步:实现“代数化”,即建立坐标系。把问题条件所有翻译成“代数方程式”(事项即“前提条件”),然后,把须要证明的事实也翻译成“代数方程式”(有待证明的事项)。吴方法的第二步:方程联立求证。

把前提条件(方承租)与待证明的方程“联立求解”,假设待证明的“方程”经过自己主动联立求解过程。变为一个恒等式,那么,这个恒等式就表示“全部前提条件”满足待证的“结论”,所以,定理得到证明,否则,问题无解。

在国际学术界,“吴方法”独树一帜,不随大流,效率最高,得到国际同仁赞扬与肯定。

经过多年人才积累,在数学定理证明机械化研究领域,研究业绩非凡,国内”吴氏学派“终于形成。请见:中科院数学机械化国家重点实验室官网。

袁萌 7月5日

转载于:https://www.cnblogs.com/llguanli/p/7103068.html

你可能感兴趣的文章
Rabbitmq集群高可用部署详细
查看>>
Mac搭建Java开发环境
查看>>
C#尝试读取或写入受保护的内存。这通常指示其他内存已损坏。
查看>>
C++标准库简介(转)
查看>>
Linux从入门到精通——控制服务
查看>>
android图片下载问题
查看>>
高并发场景下System.currentTimeMillis()的性能优化
查看>>
OpenCV&Qt学习之三——图像的初步处理
查看>>
常用命令备查
查看>>
大道至简(第四章)读后感
查看>>
SDN第四次作业
查看>>
idea连接服务器上传jar并运行
查看>>
oracle高级分组
查看>>
django--->form表单
查看>>
获取网页源代码
查看>>
一个简单的演示用的Linux字符设备驱动程序
查看>>
spi和I2c的速率
查看>>
Android 开源框架ActionBarSherlock 和 ViewPager 仿网易新闻客户端
查看>>
新技能 get —— Python 断点续传下载文件
查看>>
电商秒杀系统
查看>>