面向語義Web的動態(tài)邏輯X-DL的推理及應(yīng)用研究.pdf

1、隨著語義Web各項(xiàng)技術(shù)的發(fā)展，作為語義Web本體語言O(shè)WL的邏輯基礎(chǔ)，描述邏輯DL也得到了很大的發(fā)展。描述邏輯是一類適合于刻畫靜態(tài)領(lǐng)域知識的形式化表示工具，在軟件工程、信息系統(tǒng)等領(lǐng)域都已得到了成功的應(yīng)用。描述邏輯在具有較強(qiáng)描述能力的同時還具有可判定性的特征，同時它還具有高效的推理算法和推理工具作為支撐。
　　由于語義Web是一個動態(tài)的分散的環(huán)境，為了能更加準(zhǔn)確地刻畫和推理語義Web中的各種知識，單純的使用描述邏輯是不現(xiàn)實(shí)的，于是很

2、多研究者提出了將描述邏輯的刻畫能力從靜態(tài)領(lǐng)域擴(kuò)展到動態(tài)領(lǐng)域中去。本文是基于文獻(xiàn)提出的命題動態(tài)邏輯的描述邏輯擴(kuò)展X-DL展開研究的，其中X可替換為從ALC到SHOIQ的各種描述能力遞增的描述邏輯。由于此文獻(xiàn)中并未給出具體的算法，本文為了進(jìn)一步發(fā)揮X-DL的知識表達(dá)和推理能力，首先將X替換為描述邏輯ALC，提出ALC-DL，為其設(shè)計(jì)了可靠和完備的Tableau判定算法；其次，為其開發(fā)了有效的推理工具；最后，本文給出其Web應(yīng)用的兩個實(shí)例。本

3、文具體完成的工作如下：
　?。?）針對以上提出的X-DL缺少有效判定算法的現(xiàn)狀，首先將X替換為ALC，給出了ALC-DL的語法和語義解釋，其次給出了ALC-DL的Tableau判定算法，最后對算法的可終止性、可靠性、完備性以及復(fù)雜度等性質(zhì)進(jìn)行了證明和分析。
　?。?）針對ALC-DL的Tableau判定算法，開發(fā)了相應(yīng)的ALC-DL(Tableau)推理機(jī)軟件。為了與語義Web的環(huán)境相協(xié)調(diào)，本文還設(shè)計(jì)了ALC-DL公式對應(yīng)的