科技: 人物 企业 技术 IT业 TMT
科普: 自然 科学 科幻 宇宙 科学家
通信: 历史 技术 手机 词典 3G馆
索引: 分类 推荐 专题 热点 排行榜
互联网: 广告 营销 政务 游戏 google
新媒体: 社交 博客 学者 人物 传播学
新思想: 网站 新书 新知 新词 思想家
图书馆: 文化 商业 管理 经济 期刊
网络文化: 社会 红人 黑客 治理 亚文化
创业百科: VC 词典 指南 案例 创业史
前沿科技: 清洁 绿色 纳米 生物 环保
知识产权: 盗版 共享 学人 法规 著作
用户名: 密码: 注册 忘记密码?
    创建新词条
科技百科
  • 人气指数: 4888 次
  • 编辑次数: 1 次 历史版本
  • 更新时间: 2009-04-11
admin
admin
发短消息
相关词条
哥德尔与人工智能
哥德尔与人工智能
专家系统应用
专家系统应用
ACT模型
ACT模型
机器定理证明
机器定理证明
推荐词条
希拉里二度竞选
希拉里二度竞选
《互联网百科系列》
《互联网百科系列》
《黑客百科》
《黑客百科》
《网络舆情百科》
《网络舆情百科》
《网络治理百科》
《网络治理百科》
《硅谷百科》
《硅谷百科》
2017年特斯拉
2017年特斯拉
MIT黑客全纪录
MIT黑客全纪录
桑达尔·皮查伊
桑达尔·皮查伊
阿里双十一成交额
阿里双十一成交额
最新词条

热门标签

微博侠 数字营销2011年度总结 政务微博元年 2011微博十大事件 美国十大创业孵化器 盘点美国导师型创业孵化器 盘点导师型创业孵化器 TechStars 智能电视大战前夜 竞争型国企 公益型国企 2011央视经济年度人物 Rhianna Pratchett 莱恩娜·普莱契 Zynga与Facebook关系 Zynga盈利危机 2010年手机社交游戏行业分析报告 游戏奖励 主流手机游戏公司运营表现 主流手机游戏公司运营对比数据 创建游戏原型 正反馈现象 易用性设计增强游戏体验 易用性设计 《The Sims Social》社交亮 心理生理学与游戏 Kixeye Storm8 Storm8公司 女性玩家营销策略 休闲游戏的创新性 游戏运营的数据分析 社交游戏分析学常见术语 游戏运营数据解析 iPad风行美国校园 iPad终结传统教科书 游戏平衡性 成长类型及情感元素 鸿蒙国际 云骗钱 2011年政务微博报告 《2011年政务微博报告》 方正产业图谱 方正改制考 通信企业属公益型国企 善用玩家作弊行为 手机游戏传播 每用户平均收入 ARPU值 ARPU 游戏授权三面观 游戏设计所运用的化学原理 iOS应用人性化界面设计原则 硬核游戏 硬核社交游戏 生物测量法研究玩家 全球移动用户 用户研究三部曲 Tagged转型故事 Tagged Instagram火爆的3大原因 全球第四大社交网络Badoo Badoo 2011年最迅猛的20大创业公司 病毒式传播功能支持的游戏设计 病毒式传播功能 美国社交游戏虚拟商品收益 Flipboard改变阅读 盘点10大最难iPhone游戏 移动应用设计7大主流趋势 成功的设计文件十个要点 游戏设计文件 应用内置付费功能 内置付费功能 IAP功能 IAP IAP模式 游戏易用性测试 生理心理游戏评估 游戏化游戏 全美社交游戏规模 美国社交游戏市场 全球平板电脑出货量 Facebook虚拟商品收益 Facebook全球广告营收 Facebook广告营收 失败游戏设计的数宗罪名 休闲游戏设计要点 玩游戏可提高认知能力 玩游戏与认知能力 全球游戏广告 独立开发者提高工作效率的100个要点 Facebook亚洲用户 免费游戏的10种创收模式 人类大脑可下载 2012年最值得期待的20位硅谷企业家 做空中概股的幕后黑手 做空中概股幕后黑手 苹果2013营收 Playfish社交游戏架构

机器定理证明 发表评论(0) 编辑词条

目录

机器定理证明编辑本段回目录

 

正文编辑本段回目录

  把人证明数学定理和日常生活中的演绎推理变成一系列能在计算机上自动实现的符号演算的过程和技术,又称自动定理证明和自动演绎。机器定理证明是人工智能的重要研究领域,它的成果可应用于问题求解自然语言理解、程序验证和自动程序设计等方面。数学定理证明的过程尽管每一步都很严格有据,但决定采取什么样的证明步骤,却依赖于经验、直觉、想象力和洞察力,需要人的智能。因此,数学定理的机器证明和其他类型的问题求解,就成为人工智能研究的起点。早在17世纪中叶,莱布尼兹就提出过用机器实现定理证明的思想。19世纪后期G.弗雷格的“思想语言”的形式系统,即后来的谓词演算,奠定了符号逻辑的基础,为自动演绎推理提供了必要的理论工具。20世纪50年代,由于数理逻辑的发展,特别是电子计算机的产生和应用,机器定理证明才变为现实。A.纽厄尔和H.A.西蒙首先用探试法实现了用以证明命题逻辑中重言式的逻辑理论家系统LT。后来,开始探讨通用的机器定理证明的方法,归结原理是其中突出的例子。
  归结原理和非归结定理证明  一阶谓词逻辑的恒真性问题是不可解的,即不存在能判定一阶逻辑中任意合式公式是不是恒真式的算法,但是这个问题又是部分可解的。如果A是恒真式,那么必有算法可以证明。许多一阶逻辑的证明算法都以J.厄尔布朗定理为基础,其中以1965年J.A.鲁宾逊提出的、对于一阶逻辑是完备的证明算法即归结原理最为著名。归结原理的提出,把机器定理证明的研究推向高潮。但归结原理不依赖于领域知识,不使用依赖问题领域的探试法,证明过程冗长,不能在合理的时间和计算机存储容量内证明较为复杂的数学定理,因此人们又提出非归结定理证明方法,后来又对以探试法为基础的问题求解技术发生兴趣。与此同时还出现了因否定归结原理进而否定所有自动演绎方法的倾向。但是人工智能所要解决的问题,其信息往往是不完全的,而且即使信息完全,要对有限的但为数众多的情形一一列举,实际上也不可行,因而只有用演绎推理的方法。逻辑程序设计和日本以PROLOG为原型开发第五代计算机系统的核语言,进一步恢复了归结原理和自动演绎技术的地位。人工智能的历史表明,以认知心理学为基础的探试法和以逻辑为基础的自动演绎相辅相成,不可偏废。自动演绎与探试法等技术相结合而不用归结原理的定理证明技术,主要用于数学定理的机器证明。
  几何定理的机器证明  在数学定理机器证明中,有一类问题已有判定算法,如1951年W.斯米列夫给出的阿贝尔群判定算法,1951年A.塔斯基给出的初等几何和代数的判定算法,1960年王浩提出的命题逻辑判定算法和1976年以来吴文俊提出的初等几何和微分几何定理机器证明的理论和方法。
  非标准逻辑中的自动演绎  以经典的一阶逻辑为基础的自动演绎技术比较成熟。为了适应人工智能中复杂的推理形式,需要研究高阶逻辑和非标准逻辑中的自动演绎技术并从实用角度将这类逻辑表示形式转换成等价的经典一阶逻辑的表示形式。
  逻辑程序设计  将一阶谓词演算的子集直接作为程序设计语言的技术和方法。PROLOG语言是初步实现逻辑程序设计基本思想的第一个语言,R.科瓦尔斯基则曾对HORN子句作了过程性解释,系统地阐明了逻辑程序设计的基本理论。

 

配图编辑本段回目录

 

相关连接编辑本段回目录

→如果您认为本词条还有待完善,请 编辑词条

词条内容仅供参考,如果您需要解决具体问题
(尤其在法律、医学等领域),建议您咨询相关领域专业人士。
0

标签: 机器定理证明

收藏到: Favorites  

同义词: 暂无同义词

关于本词条的评论 (共0条)发表评论>>

对词条发表评论

评论长度最大为200个字符。