描述邏輯ALC中關(guān)于偽子概念極小改變的R-演算?

王雨暉，眭躍飛

1(中國科學(xué)院 計(jì)算技術(shù)研究所 智能信息處理重點(diǎn)實(shí)驗(yàn)室，北京 100190)

2(中國科學(xué)院大學(xué) 計(jì)算機(jī)與控制學(xué)院，北京 100049)

3(中國再保險(xiǎn)(集團(tuán))股份有限公司 信息技術(shù)中心，北京 100033)

信念修正是接受一個(gè)新信念和更新我們已有信念的過程，它的發(fā)展是哲學(xué)以及后來的計(jì)算機(jī)科學(xué)所需要的.在計(jì)算機(jī)科學(xué)中，為了更新數(shù)據(jù)庫，Doyle[1]提出了保真系統(tǒng)(truth maintenance systems)，自此，信念修正成為人工智能中的一個(gè)重要分支；而在哲學(xué)中，信念邏輯中的邏輯研究也需要考慮人類信念是如何更新和修正的.

由Alchourrón，G?rdenfors和Makinson[2?4]提出的AGM公設(shè)是一個(gè)修正算子應(yīng)該滿足的基本條件集合，它是用公式A去修正理論K，使得如果K?A?K′，則K′是K∪{A}的極大協(xié)調(diào)子集.

李未[5]給出了基于一階邏輯[6]的Gentzen-型推導(dǎo)系統(tǒng)R-演算，用來將R-構(gòu)型(configuration)Δ|Γ歸約到協(xié)調(diào)理論Δ∪Θ.Δ∪Θ是Δ∪Γ的極大協(xié)調(diào)子集，其中，Γ是協(xié)調(diào)公式集合，而Δ是協(xié)調(diào)的原子或原子公式否定的集合.在這里，Δ|Γ相當(dāng)于迭代修正Γ?Δ.因此，推導(dǎo)系統(tǒng)給出了具體的修正算子，并且證明是滿足AGM公設(shè)的.

對于描述邏輯ALC，存在這樣的 R-演算 SDL[7]:其中 R-構(gòu)型Δ|Γ可以被歸約為理論Δ∪Θ(記為)，當(dāng)且僅當(dāng)Θ是Γ關(guān)于Δ的一個(gè)集合包含極小改變(?-極小改變)(記為).這里，Θ是Γ的子理論，并且它與Δ是極大的、協(xié)調(diào)的(maximal consistent)(不是極大協(xié)調(diào)的(maximally consistent))，即:對任何理論Ξ滿足Θ?Ξ?Γ，Ξ與Δ是不協(xié)調(diào)的.在這里，我們用Δ，Θ來表示Δ∪Θ.因此，R-演算SDL關(guān)于?-極小改變是可靠的和完備的.

?-極小改變[8?10]是關(guān)于集合包含關(guān)系的，即:如果Δ|Γ?Δ，Θ在R-演算中是可證的，則Θ是Γ關(guān)于Δ的一個(gè)極小改變，如果對于任意的公式A∈Γ，Θ∪Δ?A都蘊(yùn)含有Θ∪Δ├?A.因此，我們稱Θ是Γ關(guān)于Δ的?-極大協(xié)調(diào)子集.

針對?-極小改變和R-演算SDL，我們來看具體的例子.已知Tony是一位男生，性格開朗，四肢健全，即:在我們的知識庫當(dāng)中，存在著這樣一條斷言(HavingarmsHavinglegs)(Tony).然而一次突發(fā)的事故讓Tony失去了雙腿，也使得關(guān)于Tony產(chǎn)生了一條新的事實(shí)斷言?Havinglegs(Tony).因此，我們就需要對于原有知識庫中的斷言做出修正.而按照之前R-演算SDL當(dāng)中的修正規(guī)則，我們將得到如下修正:

可以看到，經(jīng)過修正后的知識庫中將只剩下斷言?Havinglegs(Tony)，即Tony依然是有胳膊的斷言沒有了，這當(dāng)然不是我們想要的.直觀地，我們應(yīng)當(dāng)獲得這樣的修正:

顯然，SDL中的規(guī)則是會刪除掉Γ中過多的有效信息的.

因此在本文中，我們將考慮另一種極小改變的定義:

而公式A是另一個(gè)公式B的偽子公式(pseudo-subformula ofB)，如果刪除B中某些子公式可以得到A.

在描述邏輯中，我們也有類似地對于極小改變的定義[11].在描述邏輯中，我們有概念的次子概念(parasubconcepts)和偽子概念(pseudo-subconcepts)，對應(yīng)于子公式和偽子公式，并且基于此，我們給出關(guān)于-極小改變可靠和完備的R-演算TDL.需要注意的是，這里的極小改變并不是關(guān)于描述邏輯中的斷言，而是關(guān)于概念的.比如，概念集合X是概念集合Y關(guān)于概念集合Z的一個(gè)-極小改變.具體地，我們定義:

概念C是另一個(gè)概念D的偽子概念，如果通過刪除D中若干個(gè)原子概念符號可以得到C.

顯然，新的極小改變將使我們在修正的過程中，可以將修正的最小單元降到原子概念級，可以做到在修正的過程中只剔除掉那些與新事實(shí)產(chǎn)生矛盾的原子概念，從而可以最大限度地保留原有斷言中的有效信息.

相應(yīng)地，我們也將給出如下的R-演算:

R-構(gòu)型Δ|Γ在R-演算TDL中可以被歸約為理論Δ∪Θ(記為即Δ|Γ?Δ，Θ在Gentzen型推導(dǎo)系統(tǒng)TDL中是可證的)，當(dāng)且僅當(dāng)Θ是Γ關(guān)于Δ的-極小改變(記作).這是對于TDL的可靠性定理和完備性定理.

作為結(jié)果，對于上面的修正，我們在TDL將會獲得如下修正:

本文第1節(jié)給出描述邏輯ALC的基本定義，并且定義了簡化的ALC的邏輯語言和語義.第2節(jié)定義了極小改變及其相關(guān)概念和命題.第3節(jié)給出了關(guān)于斷言C(a)的R-演算，并證明了對于Δ|C(a)的推導(dǎo)規(guī)則是可靠和完備的.第4節(jié)給出了關(guān)于理論的R-演算TDL(對于斷言集合Γ的推導(dǎo)規(guī)則集合)，使得推導(dǎo)規(guī)則集合是關(guān)于極小改變可靠和完備的.最后總結(jié)全文并提出下一步工作設(shè)想.

1 預(yù)備知識

1.1 描述邏輯ALC

描述邏輯ALC由下列的邏輯語言、語法和語義組成.

描述邏輯ALC的邏輯語言包括下列符號.

· (個(gè)體)常量符號:c0，c1，…；

· 原子概念符號:A0，A1，…；

· 角色符號:R0，R1，…；

· 輔助(auxiliary)符號:(，).

概念定義為

原始斷言定義為

其中，R(c，d)和A(c)被稱為原子的.

模型M是一個(gè)序?qū)?U，I)，其中，U是非空集合(M的論域)，并且I是一個(gè)解釋，使得:

· 對任何常量符號c，I(c)∈U；

· 對任何原子概念符號A，I(A)?U；

· 對任何角色R，I(R)?U2.

概念C的解釋CI是U的一個(gè)子集，使得:

在語法中，我們使用?，∧，→，?，?來表示邏輯聯(lián)結(jié)詞和量詞；而在語義中，我們用～，&，?，A，E去表示相應(yīng)的聯(lián)結(jié)詞和量詞.

斷言φ在M中是滿足的，記為M?φ或者I?φ，如果:

1.2 偽子公式和-極小改變

1.3 偽子概念和-極小改變

2 關(guān)于單個(gè)斷言的R-演算TDL

3.1 R-演算TDL

一個(gè)斷言集合Γ的R-演算TDL:

3.2 實(shí) 例

首先來看本文開篇的那個(gè)例子.

4 總結(jié)與展望

本文給出了描述邏輯ALC中關(guān)于偽子概念()極小改變的R-演算TDL，解決了修正過程中誤刪有效信息的問題，使得在修正的過程中可以保留下盡可能多的有效信息.但修正過程中是否存在信息冗余的問題呢?

對于斷言((birdcanfly)(mammalcanwalk))(a)，其中，bird(a):a是鳥，mammal(a):a是哺乳動物，canfly(a):a會飛，canwalk(a):a會走.當(dāng)出現(xiàn)新的斷言{?bird(a)，?canwalk(a)}時(shí)，我們將有如下修正:

顯然，這是等價(jià)于?bird(a)，?canwalk(a)，(canflymammal)(a)的.

同樣地，在TDL中，我們還會有這樣的推導(dǎo):

此外，為了獲得更好的表達(dá)能力，描述邏輯在ALC的基礎(chǔ)上，通過進(jìn)一步增加構(gòu)造子的方式還得到了一些重要的擴(kuò)展.因此，我們下一步還將考慮擴(kuò)展R-演算到包含數(shù)量限制(≥nR和≤nR)的描述邏輯ALCN和帶有角色構(gòu)造子的描述邏輯ALCR中，分別針對數(shù)量限制和角色構(gòu)造子給出修正規(guī)則.而由于ALC中都是原子角色，即沒有角色的否定形式，因而在ALC中對量詞?R.C和?R.C進(jìn)行修正時(shí)，并不考慮角色R在其中的作用.但是在引入了角色構(gòu)造子之后，角色也有了它的補(bǔ)、交、并的形式，因此，我們在給出ALCR中對于角色構(gòu)造子修正規(guī)則的同時(shí)，也需要注意原先對于量詞的修正規(guī)則同樣需要修改.