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

Research and Realization of Theorem Proving Based on Combination and Replace

作　　者：于尚超[1] 李阳[1] 王鹏[1] 

机构地区：[1]解放军理工大学指挥自动化学院,江苏南京210007

出　　处：《计算机技术与发展》2012年第6期135-138,146,共5页Computer Technology and Development

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

关 键 词：机器证明 人工智能 自动推理 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]