设万维读者为首页 广告服务 技术服务 联系我们 关于万维
简体 繁体 手机版
分类广告
版主:诤友
万维读者网 > 教育学术 > 帖子
人工智能的新天地:用机器证明定理
送交者: gugeren 2017年01月08日10:07:25 于 [教育学术] 发送悄悄话

人工智能的新天地:用机器证明定理


2016年,人工智能(artificial intelligence,AI)由于阿尔法狗(AlphaGo)战胜了人类九段围棋选手而开始成为计算机领域的热词。经过半个多世纪的发展,人工智能在语音辨认、图像辨认、有偏袒游戏(partisan game,例如国际象棋和围棋)、书面语言翻译等方面都有了飞速的发展,可以与人类的智慧媲美了。


接下来,本人认为,人工智能将在自动化定理证明方面大展身手了。

自动化定理证明(Automated theorem proving,ATP)是计算机自动推理和数学逻辑的下属领域。它通过计算机程序来证明数学等学科的定理。


目前需要做的工作

1】整理和正规化数学各分支的定义、引理和定理,用类似人类自然语言的计算机语言来建立这些定义、引理和定理的数据库。这种数据库目前已经存在多种,但是规格不统一,调用不容易,内容也不规范(例如,没有显示出各个定理之间的逻辑关系)。

2】这种定理数据库,应该

--不但可以描述定义、引理和定理的内容,而且可以从某个/某些条件产生出相关的定义、引理和定理的结论,更可以提示这些条件下可能得出的其他相关的结论。

--可以把各种数学分支之间、各种定义、引理和定理之间的逻辑关系梳理清楚。


==

相关链接

自动化定理证明(Automated theorem proving,ATP)

https://en.wikipedia.org/wiki/Automated_theorem_proving


Metamath是一种写定理数据库的语言和数据库

http://us.metamath.org/


What do mathematicians think of Metamath?

https://www.quora.com/What-do-mathematicians-think-of-Metamath


0%(0)
0%(0)
标 题 (必选项):
内 容 (选填项):
实用资讯
北美最全的折扣机票网站
贝佳药业美国专利【骨精华】消关节痛、骨刺、五十肩【心血通】改善心绞痛
一周点击热帖 更多>>
一周回复热帖
历史上的今天:回复热帖
2016: 演讲通告
2016: 再见驴十八:白白红红是真粉
2015: bunny2:我对法国枪击案的看法
2015: 复旦投毒案凶手希望捐遗体(图)
2014: 【沁园春】雪(三字经版)
2014: 家长与孩子沟通期望值的平衡点为宜。
2013: 邓小平在1954年写给毛泽东的赞美诗
2013: hare:论“连系”
2012: 天蓉:脑电波之谜-40-急中生智无辜遇难