基于领域的机器定理证明的研究

《基于领域的机器定理证明的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、第40卷第2期2010年3月航空计算技术AeronauticalComputingTechniqueV01．40No．2Mal"．2010基于领域的机器定理证明的研究李凯，董春玲，赵克(西安电子科技大学机电工程学院，陕西西安710071)摘要：采用分类的思想，对领域内的证明问题进行了归纳总结、抽象，在计算机上建立了相应的模型，采用基于知识的推理技术，设计了机器定理证明的实现流程，并针对某种具体类型实现了相应的原型系统，得到了满意的结果。分类思想为具有较强客观规律问题的机器自动求解提供了思路。关键词：领域；分类；定理证明；知识推理中图分类号：TP39

2、1．6文献标识码：A文章编号：1671．654X(2010)02．0080·04引言机器定理证明，就是把人们证明定理的一般知识和规则采用适当的形式存贮到计算机中，用计算机来自动完成命题的证明，它是人工智能和知识工程的交叉研究范畴，是现代数学中一种新兴的边缘性学科，机器定理证明是人工智能的重要研究领域，它的成果可应用于问题求解、自然语言理解、程序验证和自动程序设计等方面¨’4’61。借助于逻辑推理的综合法和借助于笛卡尔坐标的代数方法，形成了几何定理机器证明研究领域的两条主要路线。代数方法不能使人满意的是，它所给出的“征明”是关于多项式的繁复的计算，人

3、难于理解其几何意义，也难于检验其是否正确。能否让计算机生成人能理解和易于检验的简明巧妙的证明，是对自动推理和人工智能领域的一个挑战性的课题¨，2J。用计算机生成几何定理可读证明的研究从上个世纪60年代以来一直在进行中【1J。目前机器定理证明主要采用数值方法进行求解，对问题能够给出证明结论，但是无法给详细的证明过程H’5J。本文采用基于知识的推理技术作为自动命题证明的开发平台，以分类思想作为系统的主线。因而提供的推导信息完全符合人们的思维习惯，这种方法不仅仅注重解题的效率，而且可以方便地向用户提供不同种类的信息服务。1系统模型由于现实问题的多样性和复

4、杂性，面向通用问题的机器证明就极其复杂。为了降低问题的复杂性，提高算法的可实现性，本文主要研究面向数学领域的机器定理证明。由于数学领域的问题具有客观性，证明的相关知识是人们已掌握的成熟知识，一般情况下可以找到合适的方法对它进行描述，也就可以设计算法在计算机上进行实现。当人们遇到复杂问题时，总是先对问题的可能解决方案进行分析，对分析的结果进行分类比较，并从中归纳出解决该类问题的普遍规律。其中分类和抽象在整个过程中起着非常重要的作用，它的正确与否直接关系着最终解决方法的复杂程度以及该方法处理问题的适应能力。知识源于人类以及其他物种的分类能力，知识是由我

5、们感兴趣的领域的分类模式组成，它提供关于现实的明显事实，同时也具备由明确事实推导出模糊事实的推理能力。分类是我们从现实世界得到论断的第一重要要素，而推理是第二重要要素pJ。本文设计的系统模型如图1所示。人机界面提供题目信息的输入和证明结果的显示；自动推理系统是该系统的核心处理部分。用户将题目和其他一些要求通过人机界面传递给输入输出转换单元，输入输出转换单元再将该信息转换成该系统所需要的形式，然后启动规则开始证明推理。推理结束后将结果的原始形收稿日期：2009—1l一20修订日期：2010．Ol一08基金项目：陕西省自然科学基金资助(2007F42)

6、作者简介：李凯(1971一)，男，陕西汉中人，副教授，硕士研究生，研究方向为知识工程，数据挖掘等。2010年3月李凯等：基于领域的机器定理证明的研究式传递给输入输出转换单元，输入输出转换单元再将原始结果及解题步骤转换成用户能看懂的普通形式，并通过人机界面显示给用户。问题一问题一问题园一图一网L．．．．．．．．．_J解答一解答一解答图1系统模型2证明问题分类由于数学中的证明问题的形式较多，有整式、分式、根式以及混合项，不可能用一种统一的方法解决所有的问题，必须对问题进行分类处理。人类知识源于对对象的分类能力，如何对对象进行合适的分类，是获取知识、解决

7、问题的关键一步，采用什么样的分类标准，是决定分类质量的重要环节。只有在对证明问题进行了有效合理的分类后，我们才能针对不同类型的题目采取不同的解题策略和方法。分类是为了减少设计的复杂度，提高设计方案的适应度。分类时也必须考虑～定的抽象性，分类太细则会显得烦琐，效率不高；分类太抽象则不利于具体实现，甚至无法实现。本文搜集了初中数学教材及辅导资料中关于证明类问题的相关素材，对其进行了分类和抽象，得到数学证明问题的基本分类如图2所示，证明中常采用的方法分类如图3所示。证明问题分类K类型ll非变量整式型lI变量整式型l变量分式型I非变量分式型II变量分式型I

8、

9、a+l／a雪_jI

10、其他图2证明问题分类图3证明方法分类3系统设计的思路作为一种知识型系统的设计，其难点不仅仅是软件的开