面向對象的幾何定理推導系統的設計與實現

摘 要：專家系統（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