面向对象的几何定理推导系统的设计与实现

摘 要：专家系统（expert system，ES）在人工智能（Artificial Intelligence，AI）中扮演着最重要也是最活跃的角色，是人工智能（AI）中最受专家重视的一个应用领域，它的出现实现了人工智能从理论研究走向实际应用，从一般的推理策略探讨转向运用专门知识的重大突破。运用特定领域的专门知识，通过推理来模拟通常由人类专家才能解决的各种复杂的、具体的问题，达到与专家具有同等解决问题能力的计算机智能程序系统。但是专家系统的设计与开发却不是一件容易的事，里面包含了大量繁琐复杂的过程，其中推理机（Inference Engine）的设计与应用就是一个难点。推理机是专家系统中实现基于知识推理的部件，是基于知识的推理在计算机中的实现，主要包括推理和控制两个方面，是专家系统中不可缺少的重要组成部分，所以推理机智的研究，有助于该领域技术知识的进一步提高与发展。

关键词：专家系统；推理机；正向推理；知识表示

1 需求分析

本课题主要解决的问题是分析专家系统中的推理机的内容和工作原理，以及推理机制的推理控制策略，并利用所设计的推理机实现对数学中几何问题的简单证明，利用专家系统在具体问题上的应用来研究如何运用推理控制策略来构建专家系统。

知识库和推理机是专家系统的核心部分，专家系统的力量来自于专家知识，推理机是专家系统必不可少的重要功能之一，专家系统的最终结论要靠推理机推出，其性能直接关系到专家系统的质量，设计一个高效的推理机可应用与各种类型的专家系统，重要性好，对知识库的维护和推理的的研究在专家系统领域具有重要的意义。

推理机是专家系统中实现基于知识推理的部件，是局域知识的推理在计算机中的实现，主要包括推理和控制两个方面，是知识系统中不可缺少的重要组成部分。

几何定理自动证明与众多应用相关，例如：机器人、计算机视觉、智能计算机辅助设计、智能计算机辅助教学等。研究人员提出了一系列研究方法，如：基于坐标的代数方法[1]，即与稽核部变量的消点法[2]等。

为了更好的理解几何定理的及其证明，本文结合面向对象的程序编程技术，实现基于面向对象的几何定理自动证明系统，该系统基于推理机的正向推理方法，结合数据库的设计，得已实现。

2 基本概念

2.1专家系统

专家系统（ExpertSystem）是一个或一组能在某些特定领域内，应用大量的专家知识和推理方法求解复杂问题的一种人工智能计算机程序。专家系统的基本结构大部分为知识库和推理机。其中知识库中存放着求解问题所需的知识，推理机负责使用知识库中的知识去解决实际问题。知识库[3][4]的建造需要知识工程师和领域专家相互合作把领域专家头脑中的知识整理出来，并用系统的知识方法存放在知识库中。

2.2推理机

2.2.1推理机

推理机根据全局数据库的当前内容，从知识库中选择相应规则，看这条规则的前提与给定的事实是否匹配。如果匹配，则得出相应的结论并将结论存入到综合数据库中，作为新的事实；反之，则启用下一条规则，再进行匹配，直到匹配成功，直至推理出问题的结论[5]。

推理机分为对象推理机、方法推理机、规则推理机，本文将不做详细介绍[6]。

2.2.2推理机的工作流程

推理机是知识库系统的核心和灵魂，本文中推理机的策略可以分为三个步骤：匹配、冲突消解、执行操作。

2.3推理

推理就是按照某种策略由已知事实根据一定的规则推导出另一事实的思维过程，在人工智能系统中，推理从不同的角度可分为：

演绎推理、归纳推理、默认推理

1.确定性推理、不确定性推理；2.单调性推理、非单调性推理；3.启发式推理、非启发式推理；4.基于知识的推理、统计推理、知觉推理。

以下将分别介绍推理的相关知识。

3 推理机制

3.1演绎推理

从已知的一般性只是出发，推理出适合于某种个别情况的结论的过程称为演绎推理。它是一种由一般到個别的推理方法，最常用的演绎推理形式是三段论式，即：“大前提、小前提、结论”。

3.2归纳推理

归纳推理的基本思想是：从已知事实中猜测出某个结论，然后对猜测的结论的正确性进行证明。

3.3确定性推理

指推理使用的证据、只是及推出的结论都是可以精确表达的，其值要么为真，要么为假，不会出现其他情况。

4 知识表示以及推理控制

4.1知识表示

推理应该选择最容易表达我们所要解决的问题的知识的方法，方便推理，易于理解与修改，常用的有产生式系统，即前提结论式，其一般格式为：

（规则编号 （IF （触发事实1）

（触发事实2）

………………..

（触发事实n））

（THEN （结论事实1）

（结论事实2）

………………..

（结论事实n）））

4.2推理的控制策略

按照推理方向的控制，推理可以分为正向推理和反向推理：

4.2.1正向推理

正向推理的算法描述：

R1.读取题目信息，根据题目初步判断所需要的规则；R2.将所需要的规则存在规则库中；R3.将读取到的信息作为事实存放在事实库中，并给定一定的顺序i=1，2，…N；R4.用规则库中的规则对读取到的第i条信息进行处理；R5.如果产生新的事实，转R6，否则，转R7；R6.将产生的新的事实存放在事实库中，i=i+1；R7.i<=N，判断结论是否在事实库中，若是，算法结束，返回结果；若否，转R4；R8.i>N，得不出结论，算法结束。endprint

算法流程图如下所示：

4.2.2反向推理

反向推理的算法描述：

（1）读取题目信息；（2）将要证明的结论作为假设存放在假设库中；将读取的事实存放在事实库中；（3）对要证明的假设，有规则库中的规则与其匹配，转（4），否则转（5）；

（4）存在事实与规则证明这个假设，则将假设存在事实库中；判断假设库是否为空，若空，算法结束；否则转（3）；（5）根据规则库中的规则，会产生新的条件，让已知假设成立，则将假设存放在事实库中，将产生的新的条件存放在假设库中，转③；

反向推理的有点是推理有目标性，执行步骤有效；缺点是正确目标选择难度大，并且错误目标导致推理失败。

5 正向推理的应用：简单的几何证明

5.1系统设计与实现

由正向推理的思想和基本的推导过程知，在系统实现时需要建立信息库，规则库，在推理引擎的驱动下，实现给定的题目的证明过程。系统的组织结构图中的核心部分如图所示：

5.2问题描述及目标的简单表示

给定的实际问题如下所示：

已知三角形ABC中，D，E为边BC上两点，AB=AC，BD=CE。

证明： AD=AE。

规则库RuleSet（引理集合）.

R1：等边对等角；R2：如果两个三角形两边对应相等，两边之间的夹角对应相等，则两个三角形全等； R3：如果两个三角形全等，则对应的边相等；R4： 如果两个三角形全等，对应的角相等。

用谓词逻辑表示已知的信息：

（2）事实库（由已知题目信息添加）

题目中给定的已知事实：

① AB=AC；②BD=CE.

5.3 推理机的设计与实现

5.3.1事实库的设计：

如下所示为建立的数据库（事实库）：

5.3.2规则库的设计：规则库（即证明所需要的规则）

建立四个属性组，分别是Rule_no（规则编号）、Rule_Name（规则名称）、Rule_condition（规则条件）、Rule_content（规则结论），建立的规则库如下图所示：

5.3.3下面进行用户操作界面的设计

在用户操作界面，用户可以直接查询事实库，也可以按照事实名字查找事实库。同时，为便于标记修改事实库，我们可以按照事实号查找相信的事实信息。题目得到的事实以及由规则推出的事实，都是可以进行查询的，得出的事实，我们都保存在事实库中，用C#来实现基本的界面设计，设计用户操作的事实库查看编辑界面如下图所示。

用同样的方法进行规则库的设计，规则库的用户操作界面同事实库界面大体相同，只是不会对规则进行修改，我们假定给定的规则都是有用且正确的，如下图所示：

5.4推导过程的设计

推导过程是由事实库与规则库相结合，进行结论的推导，推导过程的设计将最终的结果设置一个Label显示在屏幕中作为对比，当产生的事实中与其结果相同时，则结束推导，推出程序。

6 结束语：本文结合专家系统中推理机的正向推导过程，基于面向对象的语言操作实现，实现了初中几何知识的简单证明，希望能对学习机的设计有一定的帮助。推理机是专家系统的指挥中心，推理机的设计是整个专家系统的核心部分，本文分析了推理机的基础知识以及推理机的推理方法，搜索策略等。几何定理自动证明是一个重要的研究方向，具有重要的意义，本文结合面向对象编程特点，设计并实现了以及基于正向推理的集合信息自动证明原型系统，分别用事实库与规则库储存相关的信息，并利用推导过程简单地处理事实库，并得到相应的结论。

参考文献：

[1] 罗慧敏.基于消点法的几何自动推理系统实现[J].计算机应用，2008.28（11）：2984-2987

[2] 郑焕，张景中.可由用户持续发展的几何自动推理平台的推理算法[J].计算机应用，2011.31（8）：2101-2104

[3] 欧阳建权，钱跃良，李锦涛，刘任任.基于PDA的农业专家系统的知识表示与推理策略.计算机科学。2001Vol.28NO.11

[4] 欧阳建权，钱跃良，李锦涛，刘任任.基于PDA的知识库与数据库集成和通用推理算法.计算机科学。2001Vol.29NO.2

[5] 張建昌，王联国. 基于关系数据库的专家系统推理机设计. 农业网络信息. 2013 年第 2 期

[6] 郁鹏，周济，温淑红.知识处理中的推理机设计. 小型微型计算机系统Vol. 20 No. 1

作者简介：

徐晓杰 ，（1993年1-），男 ，汉，江西省上饶市 ，华南理工大学数学学院研究生 ，硕士 研究方向：非线性偏微分方程.endprint