[發(fā)明專利]一種基于重寫技術(shù)的完整性約束驗(yàn)證方法

在審

• 申請(qǐng)?zhí)枺?/td>: 202010009817.0
• 申請(qǐng)日: 2020-01-06
• 公開(kāi)（公告）號(hào): CN111241296A
• 公開(kāi)（公告）日: 2020-06-05
• 發(fā)明（設(shè)計(jì)）人: 崔仙姬;姜雨蒙
• 申請(qǐng)（專利權(quán)）人: 大連民族大學(xué)
• 主分類號(hào): G06F16/36
• 分類號(hào): G06F16/36;G06F16/33;G06F16/2453
• 代理公司: 大連智高專利事務(wù)所(特殊普通合伙) 21235
• 代理人: 馬慶朝

1.一種基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟如下：

S1、將IC公理轉(zhuǎn)化為連接查詢與not的結(jié)合，其中not在連接查詢中表示否定；

S2、將查詢主體中的分離詞分解為具有相同頭部的不同查詢，進(jìn)而轉(zhuǎn)化為連接查詢；

S3、重寫IC驗(yàn)證；

S4、根據(jù)轉(zhuǎn)換規(guī)則對(duì)DL-LiteR知識(shí)庫(kù)進(jìn)行規(guī)范化；

S5、使用算法檢驗(yàn)DL-LiteR知識(shí)庫(kù)是否滿足完整性約束。

2.如權(quán)利要求1所述的基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟S1中，對(duì)于一個(gè)KB，的連接查詢的原子at定義如下:

at←A(z)|R_a(z₁,z₂)|not A(z)|not R_a(z₁,z₂)|z₁,z₂|not z₁＝z₂

其中A和Ra分別是的原子概念和原子角色，zi是中的常數(shù)或變量。

3.如權(quán)利要求1所述的基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟S2中，用DL表示的完整性約束公理捕捉完整性約束的含義，翻譯規(guī)則如下：

其中π_c、π_r、π分別表示翻譯概念、角色和公理，主要遵循的思路是，將一個(gè)IC公理轉(zhuǎn)換為一個(gè)并集的連接查詢，當(dāng)關(guān)于的查詢?yōu)榭諘r(shí)，則IC公理被滿足，反之，則違背IC公理。

4.如權(quán)利要求1所述的基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟S3中，重寫IC驗(yàn)證步驟如下：

首先，在中的一個(gè)標(biāo)準(zhǔn)公理β適用于查詢q的原子g，如果標(biāo)準(zhǔn)公理β的和g右側(cè)具有相同概念或作用的謂詞名稱，用gr(g,β)通過(guò)使用合適的公理β來(lái)指示從原子g得到的原子，

重寫規(guī)則如下：

1、關(guān)于概念包含公理：

-如果β的左邊是一個(gè)謂詞,則gr(g,β)＝A(x)；

-如果則gr(g,β)＝P(x,y)；

-如果則gr(g,β)＝P(x,y)；

2、關(guān)于角色包含公理：

-如果g＝P(x1,x2)而且β也是或者則gr(g,β)＝P₁(x₁,x₂)；

-如果g＝P(x1,x2)而且β也是或者則gr(g,β)＝P₁(x₁,x₂)；

然后，對(duì)于中的每一個(gè)連接查詢q和標(biāo)準(zhǔn)公理β，如果q中存在一個(gè)滿足β的原子并且適用于g，則用gr(g,β)代替g，對(duì)于q中的每個(gè)原子g₁,g₂，如果g₁與g2統(tǒng)一，則g1與g2之間對(duì)q的統(tǒng)一作用最為普遍，迭代地應(yīng)用這個(gè)規(guī)則，直到中沒(méi)有公理適用于查詢q中的g。

5.如權(quán)利要求1所述的基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟S4中，每一個(gè)包含有連接概念的正包含通過(guò)規(guī)則的迭代應(yīng)用來(lái)重寫:

如果發(fā)生在中，那么用兩個(gè)斷言和來(lái)代替；中的標(biāo)準(zhǔn)公理通過(guò)以下推理規(guī)則計(jì)算所有負(fù)包含展開(kāi)：

1.如果發(fā)生在中，并且或者也發(fā)生在中,則將添加到

2.如果發(fā)生在中，并且或者也發(fā)生在中,則將添加到

3.如果發(fā)生在中，并且或者也發(fā)生在中,則將添加到

4.如果發(fā)生在中，并且或者也發(fā)生在中,則將添加到。

6.如權(quán)利要求1所述的基于重寫技術(shù)的完整性約束驗(yàn)證方法，其特征在于，步驟S5中，通過(guò)對(duì)算法IC_SATISFY進(jìn)行如下描述，輸入一組標(biāo)準(zhǔn)公理一組斷言一組IC公理如果輸出的satis滿足每個(gè)IC-axiom返回true,否則返回false。具體步驟如下：

S5.1、將satis初始化為true；

S5.2、標(biāo)準(zhǔn)化

S5.3、如果為空,返回satis,對(duì)每個(gè)IC-axiom

S5.4、將α轉(zhuǎn)化為連接查詢CQ；

S5.5、如果CQ為空，轉(zhuǎn)到步驟S5.3，對(duì)于每個(gè)cq∈CQ的查詢,CQ←CQ\cq；

S5.6、如果為空，轉(zhuǎn)到步驟S5.5，用T中的公理重寫所有cq以獲得新增查詢Qr,Qr←Qr\{α}，如果Qr為空則返回false；

S5.7、如果Qr為空，則進(jìn)入步驟S5.5，對(duì)于每個(gè)qr∈Qr的查詢，Qr←Qr\{Qr}；

S5.8、如果為空，轉(zhuǎn)到步驟S5.7，否則返回false。