王雨暉，眭躍飛

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

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

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

信念修正是接受一個(gè)新信念和更新我們已有信念的過(guò)程，它的發(fā)展是哲學(xué)以及后來(lái)的計(jì)算機(jī)科學(xué)所需要的.在計(jì)算機(jī)科學(xué)中，為了更新數(shù)據(jù)庫(kù)，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-演算，用來(lái)將R-構(gòu)型(configuration)Δ|Γ歸約到協(xié)調(diào)理論Δ∪Θ.Δ∪Θ是Δ∪Γ的極大協(xié)調(diào)子集，其中，Γ是協(xié)調(diào)公式集合，而Δ是協(xié)調(diào)的原子或原子公式否定的集合.在這里，Δ|Γ相當(dāng)于迭代修正Γ?Δ.因此，推導(dǎo)系統(tǒng)給出了具體的修正算子，并且證明是滿足AGM公設(shè)的.

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

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

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

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

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

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

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

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

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

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

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

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

作為結(jié)果，對(duì)于上面的修正，我們?cè)赥DL將會(huì)獲得如下修正:

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

1 預(yù)備知識(shí)

1.1 描述邏輯ALC

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

描述邏輯ALC的邏輯語(yǔ)言包括下列符號(hào).

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

· 原子概念符號(hào):A0，A1，…；

· 角色符號(hào):R0，R1，…；

· 輔助(auxiliary)符號(hào):(，).

概念定義為

原始斷言定義為

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

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

· 對(duì)任何常量符號(hào)c，I(c)∈U；

· 對(duì)任何原子概念符號(hào)A，I(A)?U；

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

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

在語(yǔ)法中，我們使用?，∧，→，?，?來(lái)表示邏輯聯(lián)結(jié)詞和量詞；而在語(yǔ)義中，我們用～，&，?，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í) 例

首先來(lái)看本文開(kāi)篇的那個(gè)例子.

4 總結(jié)與展望

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

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

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

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

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