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

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

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

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