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

王雨暉，眭躍飛

1(中國科學院 計算技術研究所 智能信息處理重點實驗室，北京 100190)

2(中國科學院大學 計算機與控制學院，北京 100049)

3(中國再保險(集團)股份有限公司 信息技術中心，北京 100033)

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

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

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

對于描述邏輯ALC，存在這樣的 R-演算 SDL[7]:其中 R-構型Δ|?？梢员粴w約為理論Δ∪Θ(記為)，當且僅當Θ是Γ關于Δ的一個集合包含極小改變(?-極小改變)(記為).這里，Θ是Γ的子理論，并且它與Δ是極大的、協調的(maximal consistent)(不是極大協調的(maximally consistent))，即:對任何理論Ξ滿足Θ?Ξ?Γ，Ξ與Δ是不協調的.在這里，我們用Δ，Θ來表示Δ∪Θ.因此，R-演算SDL關于?-極小改變是可靠的和完備的.

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

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

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

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

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

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

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

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

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

相應地，我們也將給出如下的R-演算:

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

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

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

1 預備知識

1.1 描述邏輯ALC

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

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

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

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

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

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

概念定義為

原始斷言定義為

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

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

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

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

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

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

在語法中，我們使用?，∧，→，?，?來表示邏輯聯結詞和量詞；而在語義中，我們用～，&，?，A，E去表示相應的聯結詞和量詞.

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

1.2 偽子公式和-極小改變

1.3 偽子概念和-極小改變

2 關于單個斷言的R-演算TDL

3.1 R-演算TDL

一個斷言集合Γ的R-演算TDL:

3.2 實 例

首先來看本文開篇的那個例子.

4 總結與展望

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

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

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

同樣地，在TDL中，我們還會有這樣的推導:

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