[1]于尚超 李阳 王鹏.基于拼凑替换的定理机器证明的研究与实现[J].计算机技术与发展,2012,(06):135-138.
　YU Shang-chao,LI Yang,WANG Peng.Research and Realization of Theorem Proving Based on Combination and Replace[J].,2012,(06):135-138.
点击复制

基于拼凑替换的定理机器证明的研究与实现()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2012年06期
页码:
135-138
栏目:
智能、算法、系统工程
出版日期:
1900-01-01

文章信息/Info

Title:
Research and Realization of Theorem Proving Based on Combination and Replace
文章编号:
1673-629X（2012）06-0135-04
作者:
于尚超 李阳 王鹏
解放军理工大学指挥自动化学院
Author(s):
YU Shang-chao;  LI Yang;  WANG Peng
Institute of Command Automation, PLA University of Science ＆ Technology
关键词:
机器证明; 人工智能; 自动推理
Keywords:
mechanical theorem proving;  artificial intelligence;  automated deduction
分类号:
TP31
文献标志码:
A
摘要:
机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景;函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势。人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,采用了逻辑推理机器证明。通过思考人脑在证明定理时的思考方式,给出了一个简单易懂的机器证明的方式。首先将证明的已知和结论形式化,将已知设为start,结果为end,已经证明的公理就是road,那么证明的过程就是从start沿着road到达end的过程。实验表明,逻辑证明通过函数式程序实现,达到了预期目的
Abstract:
Mechanical theorem proving can prevent stupid mistakes of human being. It is one of the most important aspects of artificial intelligance. It can be foreseen that after a few years this technique will be used in many fields. Functional programming language is good at theorem proving,as a result of its design idea. It is similar to mathematics. It programs the way human being often do when they do the job of theorem proving. The program can also show the detailed steps. The way of human thinking can be simulated, to realize proving of theorem. Treat what people know as ＂start＂, what people want as ＂end＂ and the acknowledged truth as ＂road＂. And the procedure to prove is to find the ＂road＂ from ＂start＂ to ＂end＂. It puts forward a simple way to realize the proving of mathematics formula. The exper- iments show that achieve the goal of theorem through the use of functional language

相似文献/References:

[1]张春飞 李万龙 郑山红.Agent技术在智能教学系统中的应用与研究[J].计算机技术与发展,2009,(05):30.
　ZHANG Chun-fei,LI Wan-long,ZHENG Shan-hong.Application and Research of Agent Technology in Intelligent Tutoring System[J].,2009,(06):30.
[2]黄长专 王彪 杨忠.图像分割方法研究[J].计算机技术与发展,2009,(06):76.
　HUANG Chang-zhuan,WANG Biao,YANG Zhong.A Study on Image Segmentation Techniques[J].,2009,(06):76.
[3]张春飞 郑山红 李万龙.基于Agent技术的医疗信息整合研究[J].计算机技术与发展,2009,(10):250.
　ZHANG Chun-fei,ZHENG Shan-hong,LI Wan-long.Research on Integration of Healthcare Enterprise Based on Agent Technology[J].,2009,(06):250.
[4]杜秀全 程家兴.博弈算法在黑白棋中的应用[J].计算机技术与发展,2007,(01):216.
　DU Xiu-quan,CHENG Jia-xing.Game- Playing Algorithm in Black and White Chess Application[J].,2007,(06):216.
[5]孙锦 冯勤超.创造力支持系统[J].计算机技术与发展,2007,(03):138.
　SUN Jin,FENG Qin-chao.Creativity Support System[J].,2007,(06):138.
[6]吉张媛 何华灿.模糊Prolog系统[J].计算机技术与发展,2006,(02):123.
　JI Zhang-yuan,HE Hua-can.Fuzzy Prolog System[J].,2006,(06):123.
[7]丁莹.研究人工智能的一条新途径[J].计算机技术与发展,2012,(03):133.
　DING Ying.A New Avenue of Researching on AI[J].,2012,(06):133.
[8]张代远[].一类新型改进的广义蚁群优化算法[J].计算机技术与发展,2012,(06):39.
　ZHANG Dai-yuan.A New Improved Generalized Ant Colony Optimization Algorithm[J].,2012,(06):39.
[9]朱志慧 李雷 种冬梅.改进的BT—SVM应用于电力系统SSA[J].计算机技术与发展,2012,(09):157.
　ZHU Zhi-hui,LI Lei,CHONG Dong-mei.Improved Binary Tree Support Vector Machine and Its Application to Power System Static Security Assessment[J].,2012,(06):157.
[10]张代远.新型样条权函数神经网络的云计算研究[J].计算机技术与发展,2013,(07):57.
　ZHANG Dai-yuan.Research on Cloud Computing for Neural Network of a New Kind of Spline Weight Functions[J].,2013,(06):57.

备注/Memo

备注/Memo:
于尚超（1986-），男，硕士，CCF会员，研究方向为人工智能
更新日期/Last Update: 1900-01-01