CAJ | 학술논문

机器定理证明可以避免人工证明容易出现的低级错误,是人工智能的重要方面,有广泛的应用前景；函数式程序设计的设计思想更加接近于数学,在定理证明方面有天然优势.人们证明逻辑推理的过程通过函数式程序实现,并将其证明的步骤显示出来,采用了逻辑推理机器证明.通过思考人脑在证明定理时的思考方式,给出了一个简单易懂的机器证明的方式.首先将证明的已知和结论形式化,将已知设为start,结果为end,已经证明的公理就是road,那么证明的过程就是从start沿着road到达end的过程.实验表明,逻辑证明通过函数式程序实现,达到了预期目的.
궤기정리증명가이피면인공증명용역출현적저급착오,시인공지능적중요방면,유엄범적응용전경；함수식정서설계적설계사상경가접근우수학,재정리증명방면유천연우세.인문증명라집추리적과정통과함수식정서실현,병장기증명적보취현시출래,채용료라집추리궤기증명.통과사고인뇌재증명정리시적사고방식,급출료일개간단역동적궤기증명적방식.수선장증명적이지화결론형식화,장이지설위start,결과위end,이경증명적공리취시road,나요증명적과정취시종start연착road도체end적과정.실험표명,라집증명통과함수식정서실현,체도료예기목적.