基于拼凑替换的定理机器证明的研究与实现

• 作者: 于尚超 李阳 王鹏
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 机器证明 人工智能 自动推理
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 135-138,146
• 分类号: TP31
• 字数: 3941字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2012.06.035

摘要

机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景；函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势.人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,采用了逻辑推理机器证明.通过思考人脑在证明定理时的思考方式,给出了一个简单易懂的机器证明的方式.首先将证明的已知和结论形式化,将已知设为start,结果为end,已经证明的公理就是road,那么证明的过程就是从start沿着road到达end的过程.实验表明,逻辑证明通过函数式程序实现,达到了预期目的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李阳	解放军理工大学指挥自动化学院	18	91	6.0	9.0
2	王鹏	解放军理工大学指挥自动化学院	5	2	1.0	1.0
3	于尚超	解放军理工大学指挥自动化学院	5	4	2.0	2.0