基于OBDD的_L（_）和ALCIO本體判定算法研究.pdf

1、描述邏輯(DL)作為一類用于知識表示的形式化工具,具有較強(qiáng)的表達(dá)能力和可判定性。近年來,隨著語義Web的興起,描述邏輯成為了知識表示領(lǐng)域的研究熱點。在關(guān)于描述邏輯的研究課題中,一個關(guān)鍵的問題是如何設(shè)計有效的推理算法。盡管Tableau-算法在描述邏輯推理中得到了廣泛并且成功的應(yīng)用,但尋求更好的推理算法一直是學(xué)術(shù)界和工業(yè)界關(guān)注的問題。
　　有序二叉決策圖(OBDD)是一種基于圖的數(shù)據(jù)結(jié)構(gòu),它是布爾函數(shù)的一種壓縮表示形式。由于有序二叉

2、決策圖能有效地表示和處理布爾函數(shù),因此在大規(guī)模模型檢測和驗證等領(lǐng)域已經(jīng)得到了成功應(yīng)用。針對OBDD的數(shù)據(jù)結(jié)構(gòu)特點,本文基于OBDD實現(xiàn)了對εL(┐)本體和ALCIO本體的一致性判定。其研究內(nèi)容和主要貢獻(xiàn)如下:
　　(1)給出了基于OBDD的εL(┐)本體判定算法。首先,利用標(biāo)準(zhǔn)化規(guī)則對TBox進(jìn)行化簡;然后,重構(gòu)了知識庫TBox模型,進(jìn)而將該模型轉(zhuǎn)化為滿足3CNF約束(每個從句含有三個變元的合取范式)的布爾函數(shù);最后,利用OBDD

3、的可滿足性操作對布爾函數(shù)進(jìn)行判定。
　　(2)給出了基于OBDD的ALICO本體判定算法,實現(xiàn)了對Nominals推理。首先,利用NNF變換和FLAT++規(guī)則對TBox進(jìn)行化簡;然后,通過模型重構(gòu)將TBox轉(zhuǎn)化為相應(yīng)的布爾函數(shù);最后,將布爾函數(shù)表示成OBDD,進(jìn)而進(jìn)行一致性判定,從理論上證明了算法的完備性、可靠性和可終止性。
　　(3)針對以上兩種推理算法,開發(fā)了相應(yīng)的原型推理系統(tǒng):DLROBDD-3CNF(EL(┐))和D