基于Tableau算法的本體模型驗證方法研究＊

蘭 天 程繼紅

（海軍航空工程學院科研部 煙臺 264001）

1 引言

本體模型的檢驗是以描述邏輯為基礎的，利用描述邏輯來實現術語及其約束關系的形式化描述。描述邏輯是人工智能領域研究的分支，是基于對象的形式化知識的表示方法，它能依據提供的構造器，在簡單的概念和關系上構造出復雜的概念和關系。描述邏輯的知識庫有兩部分組成，即∑＝〈Tbox，Abox〉，Tbox是有關概念和關系的蘊涵斷言集合，描述概念和關系的一般屬性；Abox是有關個體的實例斷言集合，斷言一個個體是某個概念的實例，或者兩個個體之間存在某種關系。因此模型的檢驗主要包括Tbox術語檢驗和Abox實例檢驗。

2 本體模型的一致性檢驗

2.1 Tbox術語檢驗推理

給定模型 M＝M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E為兩個術語，則Tbox術語檢驗包括4種：

1）術語的可滿足性檢驗：如果存在Tc與Rc的一個共同模型I滿足DI≠?，則稱D關于Tc與Rc是可滿足的，否則稱D關于Tc與Rc是不可滿足的。

術語的可滿足性用于評價術語公式對于術語集是否有意義。

2）術語的包含性檢驗：如果對任意一個Tc與Rc共同的模型I有DI?EI，則稱Tc與Rc蘊含著E包含D，記為（Tc＋Rc）╞D?E。

包含性檢驗用于評價本體中術語之間的包含關系，可以用來建立術語集的層次結構。

3）術語的等價性檢驗：如果對任意一個Tc與Rc共有的模型I有DI＝EI，則稱Tc與Rc蘊含著E包含D，記為（Tc＋Rc）╞D≡E。

等價性檢驗用于評價兩個術語是否具有相同的實例集。

4）術語的非交性檢驗：如果對任意一個Tc與Rc共有的模型I有DI∩EI＝?，則稱Tc與Rc蘊含著D與E非交，記為（Tc＋Rc）╞D?﹁E。

非交性檢驗用于判斷兩個術語是否具有相同的實例。

可滿足性問題是描述邏輯推理過程的一個核心問題，其他四種檢驗都可以轉換成可滿足性檢驗：

命題1 給定模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E為兩個術語，可以得到以下轉換：

1）（Tc＋Rc）╞D?E，當且僅當，D∩﹁E關于Tc與Rc是不可滿足的；

2）（Tc＋Rc）╞D≡E，當且僅當，D∩﹁E與﹁D∩E關于Tc與Rc是不可滿足的；

3）（Tc＋Rc）╞D?﹁E，當且僅當，D∩E關于Tc與Rc是不可滿足的。

2.2 Abox實例檢驗推理

Abox實例檢驗主要包括實例聲明的一致性檢驗和實例聲明集的一致性檢驗。

實例聲明的一致性檢驗：給定本體模型M＝〈Ta，Tc，Pd，Rc，Xd〉，若存在解釋I是實例聲明 C（a）的一個模型，則稱C（a）是一致的。若I是C（a）的一個模型，又是Tc與Rc的一個模型，則稱C（a）關于Tc與Rc是一致的。若I是Xd的一個模型，則稱Xd是一致的。若I是Xd的一個模型，又是Tc與Rc的一個模型，則稱Xd關于Tc與Rc是一致的。

實例聲明的一致性檢驗用于檢驗實例的聲明是否存在矛盾。

實例聲明集的一致性檢驗：給定本體模型M＝〈Ta，Tc，Pd，Rc，Xd〉，如果 Xd的每一個模型I都滿足實例聲明C（a），則稱Xd蘊含著C（a），記為Xd╞C（a）。

命題2 給定本體模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，Xd╞C（a），當且僅當，Xd∪｛﹁C（a）｝是不一致的。

因此，實例聲明的一致性檢驗又可以轉換為實例聲明集的一致性檢驗。

2.3 術語檢驗與實例檢驗的轉換關系

命題3 給定本體模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，C關于Tc與Rc是可滿足的，當且僅當，存在個體a，使得實例聲明集｛C（a）｝關于Tc與Rc是一致的。

由此命題可以得出術語檢驗與實例檢驗兩者不是相互獨立的，而是存在著緊密聯系的，實例聲明集的一致性檢驗與術語的可滿足性檢驗是可以相互轉換的。由命題1、命題2、命題3可知，術語的包含性、等價性、非交性檢驗以及實例聲明的一致性檢驗和實例聲明集的一致性檢驗均可約簡為可滿足性檢驗。因此，本體模型的一致性檢驗就可以簡化為術語的可滿足性檢驗。

3 可滿足性檢驗

Tableau算法最早是由Schmidt-Schau和Smolka為檢驗ALC概念的可滿足性而提出［1］，主要用于在邏輯系統中對概念的定義以及概念間的關系進行可滿足性測試，是描述邏輯推理系統的核心算法。該算法的基本思路是：通過公式來逐漸構建模型，通過自頂向下的方式來分解公式。此過程一直持續，直到找完所有可能公式。目的是為了證明沒有找到不可滿足公式的模型。

表1 本體模型可滿足性檢驗的算法規則

借鑒Tableau算法的思想，本文提出了一個本體模型術語可滿足性檢驗的基本思路：給定一個術語描述C，假定實例聲明C（x）成立，算法從初始實例聲明集A0＝｛C（x）｝開始；運用表1所示的算法規則，直到出現沖突或者沒有規則可以再用。由擴展規則可以看出，如果術語描述C中不存在符號∪，則只是向A0中添加實例聲明，不產生分支。如果術語描述C中存在符號∪，則會產生不確定的分支，只要任何一個分支是一致的，初始聲明集A0就是一致的，即術語描述C是可滿足的。檢驗流程圖見圖1。

圖1 本體模型術語可滿足性檢驗流程圖

此算法規則只能在術語描述為否定范式的情況下才能使用，所以在使用規則前，應首先使用德摩根定律將術語描述C變換為否定范式。否定范式就是否定符號只能出現在概念術語前面的術語公式。使用以下轉換我們可以將任何一個ALC術語描述轉換為否定范式：

使用規則的過程中，如果有以下3種情況的任意一種出現，我們就可以認為產生沖突：

舉例說明，給定模型的術語定義集和約束關系集分別如下：

對A?B進行驗證，就是驗證A∩﹁B是否是不可滿足的，則術語描述C為：

下面給出術語描述C的可滿足性判定過程：

說明：（2）、（3）、（4）來自于（1）使用∩規則；（5）、（6）來自于（3）使用?規則；（7）來自于（4）使用?規則；（8）、（9）來自于（7）使用∪規則。由判定過程可以看出，分支（1）、（2）、（3）、（4）、（5）、（6）、（7）、（9）存在Q（y）和﹁Q（y），此分支發生沖突；分支（1）、（2）、（3）、（4）、（5）、（6）、（7）、（8）不存在沖突，因此術語描述C是可滿足的，即給定模型是不一致的。

4 Racer推理機

4.1 Racer簡介

Racer（Renamed Abox and Concept Expression Reasoner）［2～4］是由 V.Haarslev和 R.M?ller編寫的基于描述邏輯的推理機，是一種采用描述邏輯為理論基礎的本體推理機。不僅可以當作描述邏輯系統使用，還可以用作語義知識庫系統。Racer是基于描述邏輯Tableau算法，提供了對TBox和ABox的推理功能。利用Racer的查詢推理機制可以對本體模型中的TBox和ABox的一致性進行推理，從而發現不一致信息。

Racer的主要查詢推理功能如下［5～9，11］：

（1）基本的對于本體的滿足性測試，本體的一致性通過滿足性測試來實現。本體作為建模和語義描述的工具，如果產生不一致的情況，就會使得本體應用的領域產生形式和語義的矛盾，使得在本體上的具體工作產生歧義。

（2）對于包含性的測試也可轉化為對滿足性的測試。通過對包含性的測試，使得TBox中的概念劃分了層次，形成了概念層次，便于計算概念描述的父（或者子）描述，以及計算其祖先和后代的概念描述。

（3）實例檢測可以為某些個體確定相應的概念描述。并且可以對屬于某些概念描述的個體進行分類。

（4）一些輔助的推理功能也是具體應用的重要工具。比如在知識庫中對概念名字和個體名字的檢索，與角色相關的個體對的檢索，還有角色層次的檢索，即角色的父子層次等。

4.2 實例驗證

給出一個關于海軍軍械保障的本體模型的術語定義集、約束關系集和實例聲明集分別如下：Tc＝｛AmmunitionSupport≡Ammunition∩Support，MineSupport≡Mine∩Support，MissileSupport≡Missile∩Support，TorpedoSupport≡Torpedo∩Support｝

其中，AmmunitionSupport≡Ammunition∩Support表示術語彈藥保障可以用彈藥和保障兩個術語來表示，其余用法相同。Rc＝｛LogisticSupport?Support，OperationalSupport?Support，NavalOperationalSupport?OperationalSupport，NavalOrdnanceTechnicalSupport? OperationalSupport，OrdnanceSupport?LogisticSupport，AmmunitionSupport≡OrdnanceSupport，MissileSupport?OrdnanceSupport，TorpedoSupport?Ordnance-Support，MineSupport? OrdnanceSupport，OrdnanceSupport≡OrdnanceTechnicalSupport，AmmunitionSupport?AmmunitionTechnicalSupport，MineSupport≡ MineTechnicalSupport，Missile-Support≡MissileTechnicalSupport，TorpedoSupport≡TorpedoTechnicalSupport，LogisticSupport?﹁OperationalSupport，AmmunitionSupport?﹁MissileSupport，AmmunitionSupport? ﹁ Mine-Support，AmmunitionSupport? ﹁ TorpedoSupport，MissileSupport? ﹁ MineSupport，Missile-Support?﹁TorpedoSupport，MineSupport?﹁TorpedoSupport｝

其中，LogisticSupport?Support表示后勤保障是保障的子類，OrdnanceSupport≡Ordnance-TechnicalSupport表示軍械保障和軍械技術保障是等價類，LogisticSupport?﹁OperationalSupport表示后勤保障和作戰保障是互不相交的類，其余用法相同。Xd＝｛MineSupport（xxxMineTechnicalSupport），MissileSupport（xxxMissileTestE-quipmentMeasuringSupport）， TorpedoSupport（xxxTorpedoTechnicalSupport）｝

其 中，MineSupport（xxxMineTechnicalSupport）表示xxx型水雷技術保障是水雷保障的一個實例，其余用法相同。

將以上的三個集轉換為Racer的語法來表示，其中術語定義集Tc和約束關系集Rc對應于Tbox；實例聲明集對應于Abox。代碼如下：

用Racer對Tbox和Abox分別進行一致性檢驗，將會得到如下信息：

若在約束關系集中加入約束關系AmmunitionSupport?OperationalSupport，由約束關系集中原有的約束關系OrdnanceSupport?Logistic－Support、AmmunitionSupport?OrdnanceSupport和LogisticSupport?﹁OperationalSupport，可以推理得出 AmmunitionSupport?﹁Operational－Support，與新加入的約束關系發生語義沖突。因此，如 果 將 （implies AmmunitionSupport OperationalSupport）加入到Racer推理機的Tbox代碼中，將會得到如下概念沖突信息：

若在實例聲明集中加入實例聲明MissileSupport（xxxTorpedoTechnicalSupport），由約束關系MissileSupport?﹁TorpedoSupport和實例聲明TorpedoSupport（xxxTorpedoTechnicalSupport）可以推斷出xxxTorpedoTechnicalSupport不可能是MissileSupport的一個實例，實例聲明集發生沖突。因此，如果將（instance xxxTorpedoTechnical-Support MissileSupport）加入到Abox中，將會得到如下實例沖突信息：

由以上實例可以看出，Racer可以快速準確的判斷出Tbox和Abox中存在的不一致信息，從而達到元數據模型一致性檢驗的目的。

5 結語

本文通過借鑒Tableau算法的思想，對本體模型的檢驗問題進行了研究，采用Racer推理機結合海軍軍械保障實例對基于描述邏輯的本體模型可滿足性檢驗的有效性算法進行了驗證。

［1］Schmidt-Schau M，Smolka G.Attributive concept descriptions with complements［J］.Artificial Intelligence，1991：48（1）：1-26

［2］付燕寧，金龍飛，王開鋒，等.基于本體的信息檢索系統的設計與實現［J］.計算機應用研究，2006（11）：155～157

［3］David M.Karl.RACER：Research on Antarctic coastal ecosystem rates［C］／／Deep Sea Research Part A.O-ceanographic Reasearch Papers，1991：5～7

［4］徐德智，汪志勇，王斌.當前主要本體推理工具的比較分析與研究［J］.現代圖書情報技術，2006（12）：12～15

［5］李信本，陳仲委.基于Racer和nRQL的本體查詢與推理［J］.計算機系統應用，2007（5）：33～36

［6］李景，蘇曉鷺，錢平.構建領域本體的方法［J］.計算機與農業，2003（7）：7～10

［7］劉柏嵩.面向數字圖書館的本體學習研究［J］.大學圖書館學報，2006（6）：30～34，38

［8］唐愛民，真溱，樊靜.基于敘詞表的領域本體構建研究［J］.現代圖書情報技術，2005（4）：1～5

［9］楊秋芬，陳躍新.Ontology方法學綜述［J］.計算機應用研究，2002（4）：5～7

［10］凌曉冬，劉冰，武小悅，等.基于本體的多星測控調度問題模型研究［J］.計算機與數字工程，2010，38（8）

［11］李景，孟連生.構建知識本體方法體系的比較研究［J］.現代圖書情報技術，2004（7）：17～22