基于Tableau算法的本體模型驗(yàn)證方法研究＊

蘭 天 程繼紅

（海軍航空工程學(xué)院科研部 煙臺(tái) 264001）

1 引言

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

2 本體模型的一致性檢驗(yàn)

2.1 Tbox術(shù)語檢驗(yàn)推理

給定模型 M＝M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E為兩個(gè)術(shù)語，則Tbox術(shù)語檢驗(yàn)包括4種：

1）術(shù)語的可滿足性檢驗(yàn)：如果存在Tc與Rc的一個(gè)共同模型I滿足DI≠?，則稱D關(guān)于Tc與Rc是可滿足的，否則稱D關(guān)于Tc與Rc是不可滿足的。

術(shù)語的可滿足性用于評(píng)價(jià)術(shù)語公式對(duì)于術(shù)語集是否有意義。

2）術(shù)語的包含性檢驗(yàn)：如果對(duì)任意一個(gè)Tc與Rc共同的模型I有DI?EI，則稱Tc與Rc蘊(yùn)含著E包含D，記為（Tc＋Rc）╞D?E。

包含性檢驗(yàn)用于評(píng)價(jià)本體中術(shù)語之間的包含關(guān)系，可以用來建立術(shù)語集的層次結(jié)構(gòu)。

3）術(shù)語的等價(jià)性檢驗(yàn)：如果對(duì)任意一個(gè)Tc與Rc共有的模型I有DI＝EI，則稱Tc與Rc蘊(yùn)含著E包含D，記為（Tc＋Rc）╞D≡E。

等價(jià)性檢驗(yàn)用于評(píng)價(jià)兩個(gè)術(shù)語是否具有相同的實(shí)例集。

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

非交性檢驗(yàn)用于判斷兩個(gè)術(shù)語是否具有相同的實(shí)例。

可滿足性問題是描述邏輯推理過程的一個(gè)核心問題，其他四種檢驗(yàn)都可以轉(zhuǎn)換成可滿足性檢驗(yàn)：

命題1 給定模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E為兩個(gè)術(shù)語，可以得到以下轉(zhuǎn)換：

1）（Tc＋Rc）╞D?E，當(dāng)且僅當(dāng)，D∩﹁E關(guān)于Tc與Rc是不可滿足的；

2）（Tc＋Rc）╞D≡E，當(dāng)且僅當(dāng)，D∩﹁E與﹁D∩E關(guān)于Tc與Rc是不可滿足的；

3）（Tc＋Rc）╞D?﹁E，當(dāng)且僅當(dāng)，D∩E關(guān)于Tc與Rc是不可滿足的。

2.2 Abox實(shí)例檢驗(yàn)推理

Abox實(shí)例檢驗(yàn)主要包括實(shí)例聲明的一致性檢驗(yàn)和實(shí)例聲明集的一致性檢驗(yàn)。

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

實(shí)例聲明的一致性檢驗(yàn)用于檢驗(yàn)實(shí)例的聲明是否存在矛盾。

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

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

因此，實(shí)例聲明的一致性檢驗(yàn)又可以轉(zhuǎn)換為實(shí)例聲明集的一致性檢驗(yàn)。

2.3 術(shù)語檢驗(yàn)與實(shí)例檢驗(yàn)的轉(zhuǎn)換關(guān)系

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

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

3 可滿足性檢驗(yàn)

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

表1 本體模型可滿足性檢驗(yàn)的算法規(guī)則

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

圖1 本體模型術(shù)語可滿足性檢驗(yàn)流程圖

此算法規(guī)則只能在術(shù)語描述為否定范式的情況下才能使用，所以在使用規(guī)則前，應(yīng)首先使用德摩根定律將術(shù)語描述C變換為否定范式。否定范式就是否定符號(hào)只能出現(xiàn)在概念術(shù)語前面的術(shù)語公式。使用以下轉(zhuǎn)換我們可以將任何一個(gè)ALC術(shù)語描述轉(zhuǎn)換為否定范式：

使用規(guī)則的過程中，如果有以下3種情況的任意一種出現(xiàn)，我們就可以認(rèn)為產(chǎn)生沖突：

舉例說明，給定模型的術(shù)語定義集和約束關(guān)系集分別如下：

對(duì)A?B進(jìn)行驗(yàn)證，就是驗(yàn)證A∩﹁B是否是不可滿足的，則術(shù)語描述C為：

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

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

4 Racer推理機(jī)

4.1 Racer簡(jiǎn)介

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

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

（1）基本的對(duì)于本體的滿足性測(cè)試，本體的一致性通過滿足性測(cè)試來實(shí)現(xiàn)。本體作為建模和語義描述的工具，如果產(chǎn)生不一致的情況，就會(huì)使得本體應(yīng)用的領(lǐng)域產(chǎn)生形式和語義的矛盾，使得在本體上的具體工作產(chǎn)生歧義。

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

（3）實(shí)例檢測(cè)可以為某些個(gè)體確定相應(yīng)的概念描述。并且可以對(duì)屬于某些概念描述的個(gè)體進(jìn)行分類。

（4）一些輔助的推理功能也是具體應(yīng)用的重要工具。比如在知識(shí)庫(kù)中對(duì)概念名字和個(gè)體名字的檢索，與角色相關(guān)的個(gè)體對(duì)的檢索，還有角色層次的檢索，即角色的父子層次等。

4.2 實(shí)例驗(yàn)證

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

其中，AmmunitionSupport≡Ammunition∩Support表示術(shù)語彈藥保障可以用彈藥和保障兩個(gè)術(shù)語來表示，其余用法相同。Rc＝｛LogisticSupport?Support，OperationalSupport?Support，NavalOperationalSupport?OperationalSupport，NavalOrdnanceTechnicalSupport? OperationalSupport，OrdnanceSupport?LogisticSupport，AmmunitionSupport≡O(shè)rdnanceSupport，MissileSupport?OrdnanceSupport，TorpedoSupport?Ordnance-Support，MineSupport? OrdnanceSupport，OrdnanceSupport≡O(shè)rdnanceTechnicalSupport，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≡O(shè)rdnance-TechnicalSupport表示軍械保障和軍械技術(shù)保障是等價(jià)類，LogisticSupport?﹁OperationalSupport表示后勤保障和作戰(zhàn)保障是互不相交的類，其余用法相同。Xd＝｛MineSupport（xxxMineTechnicalSupport），MissileSupport（xxxMissileTestE-quipmentMeasuringSupport）， TorpedoSupport（xxxTorpedoTechnicalSupport）｝

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

將以上的三個(gè)集轉(zhuǎn)換為Racer的語法來表示，其中術(shù)語定義集Tc和約束關(guān)系集Rc對(duì)應(yīng)于Tbox；實(shí)例聲明集對(duì)應(yīng)于Abox。代碼如下：

用Racer對(duì)Tbox和Abox分別進(jìn)行一致性檢驗(yàn)，將會(huì)得到如下信息：

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

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

由以上實(shí)例可以看出，Racer可以快速準(zhǔn)確的判斷出Tbox和Abox中存在的不一致信息，從而達(dá)到元數(shù)據(jù)模型一致性檢驗(yàn)的目的。

5 結(jié)語

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

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

［2］付燕寧，金龍飛，王開鋒，等.基于本體的信息檢索系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)［J］.計(jì)算機(jī)應(yīng)用研究，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］徐德智，汪志勇，王斌.當(dāng)前主要本體推理工具的比較分析與研究［J］.現(xiàn)代圖書情報(bào)技術(shù)，2006（12）：12～15

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

［6］李景，蘇曉鷺，錢平.構(gòu)建領(lǐng)域本體的方法［J］.計(jì)算機(jī)與農(nóng)業(yè)，2003（7）：7～10

［7］劉柏嵩.面向數(shù)字圖書館的本體學(xué)習(xí)研究［J］.大學(xué)圖書館學(xué)報(bào)，2006（6）：30～34，38

［8］唐愛民，真溱，樊靜.基于敘詞表的領(lǐng)域本體構(gòu)建研究［J］.現(xiàn)代圖書情報(bào)技術(shù)，2005（4）：1～5

［9］楊秋芬，陳躍新.Ontology方法學(xué)綜述［J］.計(jì)算機(jī)應(yīng)用研究，2002（4）：5～7

［10］凌曉冬，劉冰，武小悅，等.基于本體的多星測(cè)控調(diào)度問題模型研究［J］.計(jì)算機(jī)與數(shù)字工程，2010，38（8）

［11］李景，孟連生.構(gòu)建知識(shí)本體方法體系的比較研究［J］.現(xiàn)代圖書情報(bào)技術(shù)，2004（7）：17～22